IndisputableMonolith.Foundation.LogicAsFunctionalEquationLogic
Module that lifts the J-cost laws-of-logic package from ordinary reals onto recovered reals (LogicReal). It defines a comparison operator, the derived reciprocal cost, and the four law predicates (identity, non-contradiction, scale invariance, non-triviality), then transports each statement back to the verified real surface. Cite it when working on the foundation bridge between abstract logic carriers and the unique cost J.
claimOn recovered reals $\mathrm{LogicReal}$, a comparison operator $L$ induces a derived cost $J_L$. The predicates Identity, NonContradiction, ScaleInvariance, and NonTriviality are stated for $L$, and their conjunction is $\mathrm{SatisfiesLawsOfLogic}(L)$. Each predicate transports along $\mathrm{LogicReal}\to\mathbb{R}$ to the corresponding real statement.
background
Recognition Science forces the unique reciprocal cost $J(x)=(x+x^{-1})/2-1$ from a short list of structural laws (T5 in the forcing chain). The sibling module JcostLogic already places that cost on recovered reals: definitions live on LogicReal, and theorems reduce through LogicReal.toReal to the ordinary-real surface.
This module sits one layer up. It treats a comparison operator over recovered reals as the primitive, builds the derived cost from it, and packages the four law predicates that characterize admissible costs. The parent foundation module LogicAsFunctionalEquation supplies the real-side story; here the same vocabulary is restated on the logic carrier so that later uniqueness and forcing arguments can stay inside LogicReal until a final transport step.
Notation: $L$ is the comparison; $J_L$ the induced cost; the four predicates are the usual identity, non-contradiction, scale-invariance, and non-triviality conditions written pointwise on positive recovered reals.
proof idea
Definition-and-transport module, not a deep proof development. Comparison and derived cost are introduced as defs on LogicReal. The four law predicates and their conjunction are Prop-valued defs. Each *_to_real lemma is a one-line reduction: apply LogicReal.toReal (or the corresponding transport map from JcostLogic) and invoke the already-proved real statement from the foundation or cost surface. No independent analytic argument lives here.
why it matters in Recognition Science
Closes the logic-carrier side of the functional-equation foundation. Downstream uniqueness and forcing work that must stay on recovered reals until the end can cite SatisfiesLawsOfLogicL and the transport lemmas rather than dropping to $\mathbb{R}$ early. Ties directly to T5 J-uniqueness and the Recognition Composition Law: the same four laws that pin $J$ on the reals are now available on the abstract carrier. Used-by edges are empty in the current graph, so this is a leaf bridge module waiting on higher foundation consumers.
scope and limits
- Does not prove uniqueness of J on LogicReal; only states laws and transports them.
- Does not construct the comparison operator from first principles; it is a parameter.
- Does not discharge T5–T8 forcing steps; those remain on the real or unified-chain surface.
- Does not define mass, alpha, or dimensional forcing; foundation cost-logic only.
- Does not add new analytic inequalities beyond what JcostLogic already supplies.
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