log_generator_ne_zero
plain-language theorem explainer
A non-trivial positive real generator γ satisfies log γ ≠ 0. Workers constructing arithmetic from the Law of Logic cite this to guarantee that the multiplicative orbit starting at 1 never collapses to the fixed point. The short proof assumes the logarithm vanishes, splits on the three real roots via log_eq_zero, and obtains contradictions from positivity and the nontriviality hypothesis.
Claim. Let γ be a positive real number with γ ≠ 1. Then log γ ≠ 0.
background
Generator is the structure consisting of a positive real value together with proofs that the value is positive and not equal to 1; it is extracted from any comparison operator satisfying the Law of Logic. LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} inside the positive reals. The surrounding module ArithmeticFromLogic imports LogicAsFunctionalEquation and builds the natural-number operations directly from the functional equation that encodes the Law of Logic.
proof idea
Assume for contradiction that log γ = 0. Apply Real.log_eq_zero to obtain one of three cases: γ = 0, γ = 1, or γ = −1. The first case contradicts the positivity field of γ via lt_irrefl. The second case contradicts the nontriviality field. The third case contradicts positivity by linarith.
why it matters
The result is invoked inside embed_injective, which establishes that the map sending each LogicNat element to the corresponding power of γ is injective. This step completes the concrete embedding of the abstract LogicNat into ℝ₊ and thereby closes one link in the chain from the functional equation to ordinary arithmetic. It sits inside the T0–T8 forcing sequence that derives the eight-tick octave and three spatial dimensions from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.