the centroid-divides-medians certificate's two cofactor identities (3P.x and 3P.y) are kernel-reconstructed over Rat, needing both the fractional cast and the Rational poly x poly bridge

Identifier: F:geometry-centroid-divides-medians-kernel-checked
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.route-label-reserves-axiom-free-tally-to-kernel-lean: this fact's OWN evidence is a Kernel::add_declaration acceptance whose axiom_footprint is asserted EMPTY in the test itself -- but ADR-0601 SS2's AXIOM_FREE_CAPABLE reserves the headline axiom-free tally to proof_route kernel-lean alone, so an empty array here would be read by scripts/validate-facts.py as a claim this route cannot support., cas.does-not-prove-the-geometry: the kernel sees nine Rat variables and one algebraic identity per conclusion; that ax/ay/... are point coordinates and that the generators are 'P collinear with A, midpoint(BC)' / 'P collinear with B, midpoint(CA)' / the non-degeneracy saturation is a modelling choice made in axeyum_cas::geometry_corpus and reproduced by the translator, not discharged by the kernel., cas.geometric-conditional-not-established: the identity conclusion = sum cofactor_i*generator_i is proved for both conclusions; the implication (for all i, generator_i = 0) -> conclusion = 0 is one Rat rewrite away and is NOT taken -- no hypothesis is discharged., cas.zinv0-uninterpreted: Zinv0 is an uninterpreted universally quantified Rat variable in the reconstructed statement. The reading that it witnesses the inverse of a nonzero collinearity determinant, and hence that the theorem is vacuous on degenerate configurations, is entirely outside what the kernel term expresses -- the certificate's OWN statement field says the geometric claim is FALSE without that reading, but the kernel term does not know it., cas.characteristic-zero-specialisation: a rational-coefficient identity holds in every Q-algebra; this reconstruction is over Rat, not CReal, so nothing here says the coordinates range over the real numbers., cas.two-conclusions-proved-separately: the x and y cofactor identities are admitted as TWO SEPARATE kernel theorems (Check.geometry_centroid_cofactor_identity_x and _y), each over its own copy of the shared coordinate variables. Nothing here establishes as a single kernel-checked statement that one P simultaneously satisfies both identities., cas.translator-checked-by-evaluation-only: axeyum_cas::mvpoly::MvPoly -> this kernel's sparse RatPoly (rat_prelude::cas_geometry_frac_bridge_tests::rat_poly) is checked against numbers (tests::centroid_certificate_identity_holds_at_integer_points, including a cross-wired negative control), never by the trusted gate -- the kernel never sees an MvPoly or a Rational directly.

Recorded description

For F:geometry-centroid-divides-medians's certificate (A, B, C, P coordinates, saturation variable Zinv0 witnessing 1/collinear(A,B,C)), both of the certificate's cofactor identities -- conclusion = sum_i cofactor_i * generator_i, for centroid-x (3P.x = A.x+B.x+C.x) and centroid-y (3P.y = A.y+B.y+C.y) separately -- are reconstructed through crate::Kernel::add_declaration at symbolic universally quantified Rat variables (ax, ay, bx, by, cx, cy, px, py, Zinv0). The three generators are the two median-incidence hypotheses (each carrying genuine +-1/2 coefficients, needing the fractional-literal cast) and the Rabinowitsch saturation generator Zinv0*collinear(A,B,C) - 1; the cofactors for both conclusions include a genuinely non-constant, multi-term polynomial (needing the Rational poly x poly bridge, not just a constant-scale cast).

Formal statement

(assert (forall ((ax Rat) (ay Rat) (bx Rat) (by Rat) (cx Rat) (cy Rat) (px Rat) (py Rat) (Zinv0 Rat))
  (and (= (- (* 3 px) (+ ax bx cx))
          (+ (* c0x g0) (* c1x g1) (* c2x g2)))
       (= (- (* 3 py) (+ ay by cy))
          (+ (* c0y g0) (* c1y g1) (* c2y g2))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-reconstructed-centroid-divides-medians-cofactor-identities

Kind: kernel-term
Status: checked

Supports: 3P.x = A.x+B.x+C.x = sum_i cofactor_i*generator_i and 3P.y = A.y+B.y+C.y = sum_i cofactor_i*generator_i, each at symbolic universally quantified Rat variables, admitted by crate::Kernel::add_declaration as Check.geometry_centroid_cofactor_identity_x and Check.geometry_centroid_cofactor_identity_y. The certificate is NOT hand-copied: it is fetched from axeyum_cas::geometry_corpus::corpus() and re-certified by axeyum_cas::geometry_certify::certify, the same call path F:geometry-centroid-divides-medians's own evidence exercises. The reconstruction reuses rat_prelude::cas_partial_fractions_bridge_tests::prove_poly_combination_rat (built by an earlier lane for a different certificate, widened here from module-private to pub(super)) unchanged: the certificate's own (cofactor, generator) lists are passed to it directly, with no new proof-emitting code needed -- confirming this lane's brief that the machinery was 'already generic enough'. Each emitted normal form is asserted equal to the certificate's own conclusion polynomial BEFORE the kernel is invoked (assert_eq!(merged, concl_for_build)), and each declaration's axiom_footprint is asserted EMPTY and its kind asserted Declaration::Theorem in the same test.

Checker command

cargo test -p axeyum-lean-kernel --lib rat_prelude::cas_geometry_pair_bridge_tests::tests::geometry_centroid_cofactor_identity 2>/dev/null | /usr/bin/grep -cE '^test result: ok\. 2 passed; 0 failed'

Evidence notes

Verified both directions with /usr/bin/grep -cE explicitly (not the interactive ugrep): the real filter (matching both _x_kernel_checked and _y_kernel_checked, 'test result: ok. 2 passed') prints 1, exit 0; a fabricated test-name suffix prints 0, exit 1. Measured wall-clock, debug, uncontended: 11.33s (x alone), 18.55s (y alone), both together (cargo's own parallel scheduling) in 11.2s as part of the 7-test module sweep. Comparable to medians-concurrent's 8.14s and noticeably cheaper than rhombus's 152.79s, because although centroid's generators need the fractional cast (unlike rhombus, which is pure integer), the maximum cofactor here is only 4 terms against rhombus's 12, and no numeral magnitude larger than the certificate's own small integer coefficients is ever formed.

translator-checked-against-numbers-centroid

Kind: instance-pin
Status: checked

Supports: That rat_poly (the MvPoly -> RatPoly translator, built by an earlier lane and reused here unchanged) reads this certificate's fractional and non-constant coefficients consistently with independent evaluation, for BOTH conclusions, at a point that is NOT the triangle's own centroid -- so the cross-wired negative control (using centroid-x's cofactors against centroid-y's conclusion) is non-vacuous.

Checker command

cargo test -p axeyum-lean-kernel --lib rat_prelude::cas_geometry_pair_bridge_tests::tests::centroid_certificate_identity_holds_at_integer_points -- --exact 2>/dev/null | /usr/bin/grep -cE '^test rat_prelude::cas_geometry_pair_bridge_tests::tests::centroid_certificate_identity_holds_at_integer_points \.\.\. ok$'

Evidence notes

An earlier point choice (A=(0,0), B=(6,0), C=(0,6), P=(2,2), the actual centroid) made the cross-wired negative control vacuous -- at the centroid both generators are zero, so both cofactor combinations evaluate to zero regardless of which conclusion's cofactors are used, and the assert_ne! failed. Replaced with a generic point (verified discriminating in a throwaway, uncommitted Python script before editing Rust) where centroid-x's cofactors summed against the generators (2) genuinely differ from centroid-y's conclusion (-1).

Provenance

{
  "date": "2026-08-30",
  "established_by": "lane cas-geometry-pair: rat_prelude::cas_geometry_pair_bridge_tests (crates/axeyum-lean-kernel/src/rat_prelude/cas_geometry_pair_bridge_tests.rs)",
  "source": "F:geometry-centroid-divides-medians's own certificate, artifacts/geometry-certificates/centroid-divides-medians.json, re-fetched live from axeyum_cas::geometry_corpus rather than read from the JSON directly",
  "prior_art": [
    {
      "who": "classical Greek geometry; the centroid construction is in Archimedes' On the Equilibrium of Planes",
      "what": "the medians of a triangle meet at the centroid, which divides each in the ratio 2:1",
      "where": "standard; see e.g. Coxeter and Greitzer, Geometry Revisited (1967), section 1.4",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}