le_antisymm
plain-language theorem explainer
Antisymmetry holds for the order on LogicNat, the naturals constructed as the orbit under the generator forced by the Law of Logic. Researchers deriving arithmetic and cost functions from the functional equation cite it to close the partial-order axioms. The tactic proof extracts additive witnesses from each inequality, pushes them through the toNat equivalence, equates the images with omega, and lifts the equality back via fromNat_toNat.
Claim. Let $a,b$ belong to the inductive type LogicNat whose constructors are the zero-cost identity and the successor step. If there exists $k_1$ such that $a + k_1 = b$ and $k_2$ such that $b + k_2 = a$, then $a = b$.
background
LogicNat is the inductive type whose two constructors mirror the multiplicative orbit {1, γ, γ², …} forced by the Law of Logic; identity is the zero-cost element and step iterates the generator. The non-strict order is defined by le n m := ∃ k : LogicNat, n + k = m, so the hypotheses of le_antisymm are precisely the two existential witnesses for a ≤ b and b ≤ a. The module ArithmeticFromLogic builds Peano arithmetic on top of the functional equation imported from LogicAsFunctionalEquation; the round-trip theorems fromNat_toNat and toNat_add supply the bridge between LogicNat and ordinary Nat that the proof exploits.
proof idea
Obtain the witnesses k1 and k2 from the two le hypotheses. Apply congrArg toNat to each equality, rewrite with toNat_add, then invoke omega to conclude toNat a = toNat b. Apply fromNat to that equality and rewrite both sides with fromNat_toNat to recover a = b.
why it matters
le_antisymm supplies the missing axiom for the PartialOrder instance on LogicNat, which is required by downstream results such as agrees_on_exp_of_bounds (Cost), T5_cost_uniqueness_on_pos (Cost), unsat_positive_jcost (RSatEncoding), and defect_eq_ortho_of_subspace_case (CPM). It therefore participates in the recovery of J-cost uniqueness and the Recognition Composition Law from the arithmetic forced by the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.