RecogLattice3Cert
plain-language theorem explainer
The RecogLattice3Cert structure packages three properties of the J-cost metric on the phi-lattice: vanishing cost when the two arguments are equal and nonzero, non-negativity of domain cost for positive mass and energy, and positivity of the threshold phi minus 3/2. Lattice modelers in Recognition Science cite it to certify metric consistency before feeding into muon g-2 derivations. The definition is assembled by direct reference to the domainCost function and the upstream non-negativity theorem for J-cost.
Claim. A certificate structure consists of three properties: for every nonzero real $r$, domainCost$(r,r)=0$; for all positive reals $m,e$, $0$ ≤ domainCost$(m,e)$; and $0 <$ canonicalThreshold, where domainCost$(m,e) := J(m/e)$ with $J$ the recognition cost and canonicalThreshold $:= phi - 3/2$.
background
The module constructs a lattice on integer powers of phi with metric given by absolute J-cost, J(x) = (x + x^{-1})/2 - 1, so that the ground state sits at J=0 and the first rung at J(phi). domainCost is the two-argument wrapper J(m/e) that measures mismatch between mass and energy scales. canonicalThreshold is fixed at phi - 3/2 to mark the first excited level above the identity event.
proof idea
This is a structure definition that packages three facts already proved in the same module and its imports: domainCost r r = 0 for r ≠ 0, non-negativity of domainCost for positive arguments (via cost_nonneg), and positivity of canonicalThreshold. No tactics or reductions occur; the fields simply name the prior lemmas.
why it matters
The structure is instantiated by the cert definition and used to prove cert_inhabited, thereby closing the structural verification of the recognition lattice. It supplies the certificate required for downstream muon g-2 calculations that rely on J-cost. The construction sits inside the T5 J-uniqueness and phi-ladder steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.