Lean evidence record

Heron’s Formula — Coordinate Identity: Lean evidence

This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.

Read theorem page

Lean buildpassed

Unfinished proof stepsNone

Publication reviewsAccepted

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

noncomputable def HeronFormulaStatement : Prop :=
  ∀ p q r : Point,
    (twiceSignedArea p q r) ^ 2 =
      4 * heronRadicand (side q r) (side r p) (side p q)

Definitions used in this proposition

`Point`

abbrev Point : Type :=
  Fin 2 → ℝ

`sqDist`

def sqDist (p q : Point) : ℝ :=
  (p 0 - q 0) ^ 2 + (p 1 - q 1) ^ 2

`side`

noncomputable def side (p q : Point) : ℝ :=
  Real.sqrt (sqDist p q)

`twiceSignedArea`

def twiceSignedArea (p q r : Point) : ℝ :=
  (q 0 - p 0) * (r 1 - p 1) - (q 1 - p 1) * (r 0 - p 0)

`heronRadicand`

noncomputable def heronRadicand (a b c : ℝ) : ℝ :=
  let s := (a + b + c) / 2
  s * (s - a) * (s - b) * (s - c)

Lean wrapper declaration

The checked endpoint names the expanded proposition above. Both come from the same commit-pinned source.

theorem heronFormula :
    HeronFormulaStatement

Open main Lean file

Technical evidence record

Source identity, checker results, and assumptions

Main Lean declaration: heronFormula
Source commit: 7ff22e517713

Mechanical evidence

How Lean checked the proof

These fields support the exact Lean declaration, not a broader informal claim.

Artifact ID: artifact.known-heron-formula.coordinate.v002
Declarations covered by recorded evidence: AtlasKnownTheorems.HeronFormula.heronFormula
AtlasKnownTheorems.HeronFormula.HeronFormulaStatement
AtlasKnownTheorems.HeronFormula.heron_factor_identity
AtlasKnownTheorems.HeronFormula.coordinate_heron_factor_identity
Lean build: passed
Recorded build time: 2.5 s one machine-dependent evidence run, not a benchmark
Evidence collected: 2026-07-20 · clean-source provenance recorded
Unfinished proof check: passed
Lean toolchain: leanprover/lean4:v4.29.1
Recorded source commit: 7ff22e5177133d6e1f33590dda6ad7163487ce27
Source SHA-256: sha256:6684a874e8d475e985201e0061e0bd43aa2ba8ac62f6aad56a69f8ce7f4085fc
Statement alignment: accepted

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

Classical.choice
Quot.sound
propext

Files and machine-readable evidence

Reproduce or inspect the recorded check

Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIP Browse counted source online Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license

Review bindings

Publication reviews accepted

All four required publication-review gates are accepted for the retained presentation of this exact theorem. The review bindings are recorded separately from the Lean build and do not broaden the formal statement.

Read the publication-review details