IndisputableMonolith.Foundation.LogicAsFunctionalEquationLogic
Module that lifts the functional-equation view of classical logic from ordinary reals onto recovered reals (LogicReal). It packages a comparison operator, the cost it induces, and the four law predicates (identity, non-contradiction, scale invariance, non-triviality), plus transport lemmas back to the real surface. Anyone citing the LogicReal cost stack or the logic-as-J story uses this layer. Structure is definitional plus one-line transports through LogicReal.toReal.
claimOn recovered reals $\mathrm{LogicReal}$, a comparison operator $L$, the induced cost $J_L$, and predicates Identity, NonContradiction, ScaleInvariant, NonTrivial; together $L$ satisfies the laws of logic. Each law transports along $\mathrm{LogicReal}\to\mathbb{R}$ to the corresponding real statement.
background
Recognition Science treats classical logical structure as forced by a reciprocal cost functional equation rather than as a free axiomatic choice. The companion module LogicAsFunctionalEquation develops that story on ordinary reals; JcostLogic supplies the canonical reciprocal cost $J$ on recovered reals as a transport mirror of JcostCore, with proofs reduced through LogicReal.toReal.
This module sits at that interface. It introduces a comparison operator over recovered reals, derives a cost from it, and names the four law predicates that encode identity, non-contradiction, scale invariance, and non-triviality on LogicReal. The local convention matches JcostLogic: definitions live on the recovered type; theorem content is discharged by transport to the already-verified real surface.
proof idea
Definition-and-transport module, not a deep proof development. Comparison and derived-cost objects are declared on LogicReal. The four law predicates and the bundled SatisfiesLawsOfLogic package are Prop-level interfaces on that type. Each *_to_real lemma is a one-line transport: apply LogicReal.toReal and invoke the corresponding real-side fact from the functional-equation and Jcost stacks. No independent analytic argument is carried on LogicReal itself.
why it matters in Recognition Science
Closes the LogicReal side of the "logic as functional equation" bridge in the Foundation layer. Downstream work that needs logical laws or comparison structure on recovered reals (rather than bare $\mathbb{R}$) depends on this packaging; without it, the JcostLogic cost surface would lack a matching logical interface. In the broader RS forcing chain the move matters because T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law are stated in cost language: having identity, non-contradiction, scale invariance, and non-triviality available on the same carrier keeps the logical and cost stories aligned. No used-by edges are recorded yet; the module is infrastructure for that alignment rather than a leaf theorem.
scope and limits
- Does not prove uniqueness of $J$ or the RCL; those live upstream on the real surface.
- Does not derive T5–T8 forcing steps; only supplies LogicReal logical interfaces.
- Does not construct LogicReal itself; assumes the recovered-real carrier from imports.
- Does not assert physical constants, mass ladders, or eight-tick structure.
- Transport lemmas do not add new analytic content beyond real-side facts.
depends on (2)
declarations in this module (14)
-
abbrev
ComparisonOperatorL -
def
derivedCostL -
def
transportComparison -
def
IdentityL -
def
NonContradictionL -
def
ScaleInvariantL -
def
NonTrivialL -
structure
SatisfiesLawsOfLogicL -
theorem
identityL_to_real -
theorem
nonContradictionL_to_real -
theorem
scaleInvariantL_to_real -
theorem
nonTrivialL_to_real -
theorem
lawsL_to_real -
theorem
RCL_is_unique_functional_form_of_logicL