le_trans
plain-language theorem explainer
Transitivity of the order on LogicNat follows from the definition of ≤ via additive witnesses together with associativity of addition. Researchers deriving causal reachability bounds or proving local-to-global minimality of action functionals cite this when chaining inequalities. The proof is a direct term-mode construction that obtains the two witnesses, forms their sum, and reassociates via the upstream add_assoc lemma.
Claim. Let $a,b,c$ belong to the logic naturals. If $b=a+k_1$ for some $k_1$ and $c=b+k_2$ for some $k_2$, then $c=a+k$ for $k=k_1+k_2$.
background
LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator γ and containing the multiplicative identity. Addition on LogicNat is defined recursively by the usual Peano rules, with the zero element identified with identity. The present lemma sits inside the module that extracts ordinary arithmetic from the Recognition functional equation; it depends on the already-established associativity of this addition, proved by induction on the third argument.
proof idea
Obtain the additive witnesses k1 from the first hypothesis and k2 from the second. Form the combined witness k1 + k2. Apply add_assoc to rewrite the target equality as (a + k1) + k2 and substitute the two given equalities.
why it matters
The result is invoked in more than forty downstream statements, among them actionJ_local_min_is_global (which upgrades local action minima to global ones via convexity), frequency_bound_nonneg (which extracts non-negativity from frequency bounds), and inBall_mono together with ballP_subset_inBall (which propagate reachability inside causal balls). It therefore supplies the elementary order arithmetic required by the causality and analysis layers that rest on the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.