one_def
plain-language theorem explainer
The declaration states that the numeral 1 in LogicNat equals the successor of zero. Researchers deriving arithmetic primitives from the logic functional equation cite it when unfolding basic operations in the Recognition Science foundation. The proof reduces to reflexivity once the notations for zero as the identity constructor and successor as the step constructor are expanded.
Claim. In the inductive type LogicNat, the element denoted $1$ satisfies $1 = succ(0)$, where $0$ is the identity constructor and $succ$ applies the step constructor.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity in the orbit) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. The successor function is defined directly as succ n := step n, and zero is the identity element. This theorem belongs to the module that extracts Peano-style arithmetic as theorems from the Law of Logic rather than positing axioms.
proof idea
The proof is a one-line reflexivity application. Once the numeral notation for 1, the definition of zero as identity, and the definition of succ as step are unfolded, the two sides are identical by construction.
why it matters
This supplies the first nontrivial numeral in the arithmetic layer built from the logic functional equation, supporting later definitions such as addition and the induction principle in the same module. It sits inside the foundation that feeds the forcing chain from T0 onward and the phi-ladder constructions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.