phi_code_distance_pos
plain-language theorem explainer
The φ-code distance is strictly positive. Researchers modeling error correction in Recognition Science cite this to confirm that the φ-ladder supplies a positive code distance, a prerequisite for non-trivial fault tolerance in ledger dynamics. The proof is a one-line wrapper that unfolds the definition and invokes the general J-cost positivity lemma with the elementary facts that φ > 0 and φ ≠ 1.
Claim. $0 < d_φ$, where $d_φ$ is the code distance induced by the golden ratio φ through the J-cost function on the φ-ladder.
background
In the Error Correction module, recognition defects are deviations from the J=0 ground state, defect energy is the J-cost of such a deviation, and the φ-ladder structure supplies the code distance for the stabilizer-code interpretation of the ledger. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1; its proof rewrites Jcost as a square divided by a positive denominator. The module frames the 8-tick cycle as the error-correction period and links RS thermodynamics to quantum error correction via the ledger as stabilizer code.
proof idea
The term proof unfolds phi_code_distance and applies Jcost_pos_of_ne_one. It discharges the two side conditions by quoting Foundation.PhiForcing.phi_pos for positivity and (Foundation.PhiForcing.phi_gt_one).ne' for inequality to 1.
why it matters
This result places the positivity of the φ-code distance inside the error-correction viewpoint of RS thermodynamics, supporting the claim that ledger dynamics implements fault tolerance. It fills the code-distance slot required by the φ-ladder (T6–T7) and the eight-tick octave, and it is a prerequisite for any later statement of the fault-tolerance threshold. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.