cert_inhabited
plain-language theorem explainer
The theorem establishes existence of a certificate for the three-dimensional recognition lattice by exhibiting an explicit construction. Researchers deriving physics from the J-cost functional equation would cite this to confirm the lattice axioms are consistent. The proof is a direct term that applies the structure constructor to a prior definition of the certificate.
Claim. There exists a certificate for the recognition lattice such that the cost function vanishes for equal nonzero real arguments, remains nonnegative for positive mass and energy arguments, and the canonical threshold is positive.
background
The module sets up a lattice on the set of integer powers of phi, with J-cost J(phi to the power of the difference) serving as the distance metric. The ground state sits at exponent zero where cost is zero. The certificate structure requires three properties on the domain cost function and the threshold: vanishing at equal nonzero points, nonnegativity on positive arguments, and strict positivity of the threshold.
proof idea
The proof is a one-line term that applies the structure constructor to the term defining the certificate.
why it matters
This result confirms the lattice axioms are satisfiable inside the Recognition Science framework and closes the structural theorem for the J-cost lattice. It supports the forcing chain steps that derive D equals 3 and the eight-tick octave from the Recognition Composition Law. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.