IndisputableMonolith.Gravity.SevenGaps.Gap5O6ChartInvariant
Module packaging the O(6) chart-invariant for Gap 5 in the gravity seven-gaps campaign: among ADM kinetic coefficients, the product is fixed by recognition rigidity while the ratio remains free. Gravity and constraint-sector workers cite it when separating chart artifacts from genuine invariants. The argument is algebraic: product uniqueness plus an explicit free-ratio family.
claimFor ADM kinetic coefficients $(A,B)$ on the constraint sector, recognition rigidity fixes the product $A\cdot B$ as a chart-invariant, while the ratio $A/B$ is free: it is not determined by the composition law and attains every positive value under admissible reparametrizations.
background
Gap 5 sits in Campaign 2 Track A on the constraint sector. Upstream work (Gap5ReparamAttackOnConstraintSector) attacks field-independence of the kinetic weight via the Recognition Composition Law (RCL): $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, as derived in HKT kinetic-from-recognition-cost §8. The companion paper printed a falsifier (a weight not satisfying the composition law yet still field-independent) that this track is meant to close or refute.
This module isolates the O(6)-chart content of that attack. ADM coefficients encode the kinetic pairing on the constraint surface. The local claim is that rigidity delivers a coefficient relation: the product of the two coefficients is an invariant of the recognition structure, whereas the ratio is a pure chart degree of freedom. Sibling lemmas name the pieces: product determined, ratio not determined, ratio takes every value, and recognition transfers sign to the gradient.
proof idea
Definition-plus-lemma module, not a single monolithic proof. It introduces ADMCoefficients and proves four structural facts: the product is uniquely fixed; the ratio is not fixed by the recognition hypotheses; an explicit family shows the ratio attains every positive value; and recognition pushes sign information onto the gradient. The headline theorem gap5_o6_ratio_is_free_product_is_the_invariant (with a _holds wrapper) packages those facts as the coefficient relation the rigidity theorem delivers. Imports only the reparametrization-attack module; no further external lemmas are required beyond that sector setup.
why it matters in Recognition Science
In the seven-gaps gravity program, Gap 5 asks which pieces of the kinetic sector are forced by recognition versus which are gauge/chart. This module answers for the O(6) chart: product invariant, ratio free. That split feeds the reparametrization attack on the constraint sector and supports the broader claim that RCL-forced kinetic structure is field-independent without over-constraining chart data.
Downstream use is presently empty in the graph (used_by_count: 0), so the module is a leaf packaging step: it records the invariant the rigidity theorem actually yields so later constraint-sector and QG papers can cite a named Lean object rather than an informal coefficient relation. It touches the paper falsifier printed in the QG constraint-sector recognition premise: any purported counterexample weight must still respect this product invariant if it claims to live in the same chart class.
scope and limits
- Does not prove full field-independence of the kinetic weight; only the product/ratio split for ADM coefficients.
- Does not discharge the paper falsifier for weights outside SatisfiesCompositionLaw.
- Does not fix absolute normalization of either coefficient, only their product.
- Does not treat non-ADM kinetic pairings or charts outside the O(6) setup.
- Does not yet appear as a dependency of a parent theorem in the import graph.