decorated_geometry.lean

-- Auto-generated by ``deppy.lean.sidecar_certificate``.
-- Module: examples.decorated_geometry
-- Foundations: 5; specs: 1; axioms: 2; proofs: 0.
-- Library: examples.decorated_geometry
--
-- Trust chain: Foundations (mathematical facts) ⟶ Sidecar axioms
-- (claims about library behaviour) ⟶ Theorems (real proof
-- terms — Eq.trans / And.intro / rfl / Foundation.symm.trans
-- — type-checked by Lean's kernel).

/-! ## Annotation-driven concrete preamble (CONCRETE-PROPS) -/

-- Types, method signatures, and concrete Props
-- assembled from .deppy ``binders:`` / ``function:`` /
-- ``property:`` / ``code_types:`` annotations.  PSDL
-- tactics elaborate against these (not against opaque
-- Int symbols).

-- ── Concrete types from verify-block binders (definitional aliases to Int) ──
abbrev Point : Type := Int

-- ── User-declared code-type signatures (from .deppy code_types:) ──
axiom sqrt : Int → Int
axiom sum_zip_sub_sq : Point → Point → Int

-- ── Concrete Foundation Props (assembled from foundation statements) ──


/-! ## Mechanization preamble — vocabulary from .deppy axioms -/

-- Opaque types and operations declared from the union of all GROUNDED
-- axiom statements.  Foundation axioms below are stated as concrete
-- Lean Props over this vocabulary; non-grounded axioms fall back to
-- opaque Props.

-- Class-prefixed methods and constructors (derived)
-- Methods/ctors are ``def := fun _ => 0`` so ``unfold``
-- + ``omega`` / ``rfl`` can close arithmetic claims
-- against the placeholder.  The semantic body (from
-- deppy.lean.body_translation) is emitted separately
-- in the 'Body links' section below.
def Point_distance (_0 : Int) (_1 : Int) : Int := 0

-- Tuple constructors (used when an axiom contains a tuple literal)
def Pair2_mk (_0 _1 : Int) : Int := 0
def Pair3_mk (_0 _1 _2 : Int) : Int := 0
def get (_0 _1 : Int) : Int := 0


/-! ## Foundations — generic mathematical facts (trust surface) -/

-- Each foundation's Prop is now *concrete*: it states an
-- arithmetic identity over Int that Lean's elaborator
-- can unfold and unify with goal types.  Where the
-- statement is true unconditionally over Int we declare
-- the foundation as a real ``def := True`` (admitted by
-- ``trivial``); where it requires real arithmetic
-- support beyond Lean core we keep the opaque shape.

axiom Real_sqrt : Int → Int

-- Foundation: Real_add_comm
-- Statement: a + b == b + a
def Foundation_Real_add_comm_prop : Prop := ∀ (a b : Int), a + b = b + a
theorem Foundation_Real_add_comm : Foundation_Real_add_comm_prop := by unfold Foundation_Real_add_comm_prop; intros; omega

-- Foundation: Real_sqrt_nonneg
-- Statement: sqrt(x) >= 0 when x >= 0
opaque Foundation_Real_sqrt_nonneg_prop : Prop
axiom Foundation_Real_sqrt_nonneg : Foundation_Real_sqrt_nonneg_prop

-- Foundation: Real_sqrt_sq_nonneg
-- Statement: sqrt(x)**2 == x when x >= 0
-- Citation:  Pythagoras
def Foundation_Real_sqrt_sq_nonneg_prop : Prop := True
theorem Foundation_Real_sqrt_sq_nonneg : Foundation_Real_sqrt_sq_nonneg_prop := trivial

-- Foundation: Real_sub_sq_swap
-- Statement: (a - b)**2 == (b - a)**2
opaque Foundation_Real_sub_sq_swap_prop : Prop
axiom Foundation_Real_sub_sq_swap : Foundation_Real_sub_sq_swap_prop

-- Foundation: Real_sum_of_squares_nonneg
-- Statement: sum of nonneg terms == 0 iff each term == 0
def Foundation_Real_sum_of_squares_nonneg_prop : Prop := True
theorem Foundation_Real_sum_of_squares_nonneg : Foundation_Real_sum_of_squares_nonneg_prop := trivial

/-! ## Sidecar axioms — claims about library behaviour -/

-- Axiom: dist_nonneg
-- Grounding: GROUNDED
-- Target: examples.decorated_geometry.Point.distance; Module: examples
-- Statement (Python): Point.distance(p, q) >= 0
-- Concrete Lean Prop (mechanized from .deppy):
def Sidecar_dist_nonneg_prop : Prop := ∀ (p q : Int), ((Point_distance p q) ≥ 0)
axiom Sidecar_dist_nonneg : Sidecar_dist_nonneg_prop

-- Axiom: dist_symmetric
-- Grounding: GROUNDED
-- Target: examples.decorated_geometry.Point.distance; Module: examples
-- Statement (Python): Point.distance(p, q) == Point.distance(q, p)
-- Concrete Lean Prop (mechanized from .deppy):
def Sidecar_dist_symmetric_prop : Prop := ∀ (p q : Int), ((Point_distance p q) = (Point_distance q p))
axiom Sidecar_dist_symmetric : Sidecar_dist_symmetric_prop

/-! ## Spec guarantees (informational) -/

-- Spec: examples.decorated_geometry.Point
--   guarantee: Distance is non-negative.
--   guarantee: Distance is symmetric: d(p, q) == d(q, p).
--   axioms: dist_nonneg, dist_symmetric

/-! ## Foundation discharge — deppy.core.kernel Z3 backend -/

-- 2/2 arithmetic foundations discharged at TrustLevel.Z3_VERIFIED.
--   ✓ Real_add_comm via Z3: a + b == b + a
--   – Real_sqrt_nonneg (non-arithmetic, admitted)
--   – Real_sqrt_sq_nonneg (non-arithmetic, admitted)
--   ✓ Real_sub_sq_swap via Z3: (a - b)**2 == (b - a)**2
--   – Real_sum_of_squares_nonneg (non-arithmetic, admitted)

/-! ## Verified code properties — .deppy ``verify`` blocks -/

-- 1/2 verify blocks accepted by deppy.core.kernel.ProofKernel.verify.

-- ── verify distance_verify ── (function: examples.decorated_geometry.Point.distance)
--   property:   Point.distance(p, q) >= 0
--   foundation: Real_sqrt_nonneg
--   source SHA256: 30488825f34252b4…
--   body translation: sorry(0)
--   note: ast.parse failed: unexpected indent (<unknown>, line 1)

-- ── verify distance_symmetric_verify ── (function: examples.decorated_geometry.Point.distance_symmetric)
--   property:   Point.distance(p, q) == Point.distance(q, p)
--   foundation: Real_sub_sq_swap
--   source SHA256: 1b225b61eb3b72cb…
--   body translation: EXACT
--   kernel.verify: success=True trust=STRUCTURAL_CHAIN axioms_used=[]
--   kernel.message: Trans: middle term inferred structurally
--   note: ProofTerm shape: Unfold+AxiomInvocation
-- verify distance_symmetric_verify
-- function:  examples.decorated_geometry.Point.distance_symmetric
-- property:  Point.distance(p, q) == Point.distance(q, p)
-- foundation: Real_sub_sq_swap
-- source SHA256: 1b225b61eb3b72cb…
-- deppy.body_translation: EXACT
-- ProofKernel.verify accepted: Unfold(Point_distance_symmetric, AxiomInvocation(Real_sub_sq_swap))
-- TrustLevel: STRUCTURAL_CHAIN; axioms_used: []
def Verified_distance_symmetric_verify_property : Prop := ∀ (p : Point) (q : Point), ((Point_distance p q) = (Point_distance q p))
theorem Verified_distance_symmetric_verify : Verified_distance_symmetric_verify_property := by
  -- Lean tactic synthesised by deppy: unfold the concrete
  -- property + every mechanized callee (axiom-backed names
  -- guarded by ``try``), then close with the first
  -- arithmetic / definitional tactic that succeeds.
  try unfold Verified_distance_symmetric_verify_property
  try unfold Point_distance
  intros
  try unfold Verified_distance_symmetric_verify_property
  try unfold Point_distance
  first
    | exact Foundation_Real_sub_sq_swap
    | rfl
    | omega
    | decide
    | trivial
    | simp
    | sorry  -- fallthrough: deppy verified, Lean disagrees
  -- ProofKernel verdict (deppy): accepted as Unfold(<func>, AxiomInvocation(Real_sub_sq_swap))