Leibniz's centroid formula over the constructed reals: |PA|^2+|PB|^2+|PC|^2 = 3|PG|^2 + (|GA|^2+|GB|^2+|GC|^2) in CPoint

Identifier: F:geometry-leibniz-centroid-over-constructed-reals
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any four points P, A, B, C of the plane CPoint = CReal x CReal over the constructed (Bishop) reals, with G = CPoint.centroid A B C = (A+B+C)/3, the sum of squared distances from P to the three vertices equals three times the squared distance from P to the centroid plus the sum of squared distances from the centroid to the vertices. Equality is CReal.Equiv, a DEFINED Prop relation on the setoid of regular rational sequences, NOT Eq. The statement is unconditional: no non-degeneracy, no collinearity exclusion, and P is arbitrary and need not lie in any particular position relative to the triangle. The factor 3 appears additively (|PG|^2 + |PG|^2 + |PG|^2), not as multiplication by a constructed scalar, so the statement itself does not depend on the existence of 1/3 -- though the centroid it is stated about does, and that reciprocal is witnessed (see notes).

Formal statement

((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CPoint) -> CReal.Equiv (CReal.add (CPoint.distSq x0 x1) (CReal.add (CPoint.distSq x0 x2) (CPoint.distSq x0 x3))) (CReal.add (CReal.add (CPoint.distSq x0 (CPoint.centroid x1 x2 x3)) (CReal.add (CPoint.distSq x0 (CPoint.centroid x1 x2 x3)) (CPoint.distSq x0 (CPoint.centroid x1 x2 x3)))) (CReal.add (CPoint.distSq (CPoint.centroid x1 x2 x3) x1) (CReal.add (CPoint.distSq (CPoint.centroid x1 x2 x3) x2) (CPoint.distSq (CPoint.centroid x1 x2 x3) x3))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 0 direct dependents

Evidence

kernel-CPoint.centroid_dist_sq

Kind: kernel-term
Status: checked

Supports: `CPoint.centroid_dist_sq` is admitted by the kernel with exactly the type in formal.statement. The proof expands each vertex distance around the pivot G via `dot_self_sub`, uses a new `triple_sub_sum_zero` (the three vertex-to-centroid vectors sum to zero, from 3G ~ A+B+C) and `dot_zero_right`, and reassociates twelve terms through the file's existing SumTree / flatten_sum_tree / reorder_right_chain / concat_right_chains machinery.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests::centroid_dist_sq_statement_is_exact -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Re-derives from source every run: rebuilds CPointPrelude, re-typechecking `Scalar.three`, `inv3`, `threePosBound`, `centroid`, `centroid_median` and `centroid_dist_sq` through `add_declaration`, then compares the rendered type character for character. Anchored on the exact `1 passed; 0 failed` count; verified that substituting a non-existent test name makes the identical command exit 1 rather than 0, so a silently-empty filter cannot read as success.

footprint-CPoint.centroid_dist_sq

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] -- the theorem, the centroid it is stated about, and the witnessed reciprocal 1/3 beneath it are all checked declarations with an empty `Kernel::axiom_footprint`. The `cpoint` prelude's trusted surface is 0: no Axiom, no Opaque, no Quotient.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests::every_theorem_here_is_axiom_free -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Counting Declaration::Axiom alone would not suffice (Opaque has no proof body and Quotient admits Quot.sound); axiom_footprint covers all three. Presence matters as much as the footprint -- axiom_footprint of a name interned but never declared is vacuously empty -- so the statement test above, which fetches the declaration from the environment and panics if absent, is the companion check.

Provenance

{
  "date": "2026-08-23",
  "established_by": "lane agent-capability-assurance (2026-08-23), via a dispatched geometry lane: crates/axeyum-lean-kernel/src/creal_point.rs, `CPoint.centroid_dist_sq`, a kernel theorem over CReal (the constructed reals, ADR-0512) admitting with an empty axiom_footprint.",
  "source": "classical; coordinatised by the geometry lane",
  "prior_art": [
    {
      "who": "Gottfried Wilhelm Leibniz",
      "what": "the relation between the sum of squared distances to the vertices of a triangle and the distance to its centroid",
      "year": 1700,
      "where": "attributed in the standard literature as Leibniz's formula; commonly stated for an arbitrary point and the barycentre",
      "attribution": "conventional attribution only. This lane did not consult a primary source, and the date is approximate; the identity is a special case of a general barycentric relation and its first appearance is not established here."
    }
  ]
}