lt_trans
plain-language theorem explainer
Transitivity of the strict order on LogicNat, the naturals forced by the functional equation of logic. Cited in downstream positivity arguments for constants and bounds in modules such as CostAlgebra, LedgerAlgebra, and applied chemistry and cosmology results. The proof rewrites the strict inequalities via the successor characterization then chains two applications of non-strict transitivity with the successor inequality inserted.
Claim. Let $a, b, c$ belong to the inductive type generated by the identity and successor constructors that mirrors the multiplicative orbit. If $a$ is strictly less than $b$ and $b$ is strictly less than $c$, then $a$ is strictly less than $c$.
background
LogicNat is the inductive type whose constructors identity and step encode the zero-cost element and successive iterations of the generator, reproducing the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ. The relations < and ≤ are defined on this type via the successor and addition operations already constructed in the same module. The result depends on le_trans (non-strict transitivity obtained by adding the witnessing increments), le_succ (n ≤ succ n witnessed by adding zero), and lt_iff_succ_le (strict inequality equivalent to successor ≤ target).
proof idea
Rewrite the two hypotheses and the goal with lt_iff_succ_le to replace each strict inequality by a non-strict one involving the successor. Apply le_trans to the resulting pair, inserting the intermediate inequality le_succ b to connect succ b with the second hypothesis.
why it matters
The lemma supplies the ordered arithmetic needed to chain inequalities throughout the Recognition framework, appearing in defectDist_no_global_quasi_triangle (Proposition 2.6), Cycle structures, angle_bias, gamma_pos, w8_pos, and bounds such as alpha_over_pi_bounds. It closes a basic step in the arithmetic layer derived from the logic functional equation, supporting the phi-ladder and eight-tick constructions without introducing extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.