identity_terminal_kills_log
plain-language theorem explainer
Logarithm of the identity terminal vanishes. Researchers formalizing the EML compiler gate from oriented recognition coordinates cite this when the log channel receives the unit state. The proof is a one-line simplification that applies the standard logarithm property at unity.
Claim. The natural logarithm satisfies $log 1 = 0$.
background
The module establishes the RS/EML bridge by showing that an oriented recognition ledger carries an additive logarithmic coordinate before reciprocal symmetrization. The chart maps between multiplicative ratios and this additive coordinate are the exponential and logarithm functions, while the oriented ledger combiner is subtraction. This induces the two-input compiler gate eml x y = exp x - log y.
proof idea
The proof is a one-line simplification that invokes the standard property that the logarithm of unity is zero.
why it matters
This result closes the log channel at the identity terminal, enabling the oriented compiler gate eml x y = exp x - log y. It supports the recovery of the logarithm from the EML structure in the same module. In the Recognition Science framework it confirms that the additive log coordinate is well-defined at the J-minimum point, consistent with the forcing chain where the identity sits at the base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.