pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure

show as:
view Lean formalization →

This module defines the truth-evaluable comparison as the minimal semantic structure required to evaluate statements about positive-ratio comparisons. Researchers formalizing the logic-as-functional-equation foundation cite it to anchor the transition from mismatch magnitudes to operator conditions. The module supplies lemmas that convert its four semantic fields into the algebraic conditions (L1) through (L4).

claimA truth-evaluable comparison is the minimal structure with four fields that encode the requirements for evaluating positive-ratio comparisons, translated into algebraic conditions (L1)--(L4).

background

The module sits inside the LogicAsFunctionalEquation development and rests on the canonicality module. That upstream result states: once a comparison operator is read as a magnitude of mismatch, the operator-level conditions are the canonical structural content of that reading. The truth-evaluable comparison supplies the semantic language whose four fields are then converted by lemmas into the algebraic package (L1)--(L4).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the semantic foundation that feeds the counted-once comparison module (affine combiner for each constituent counted once) and the finite logical comparison module (finite pairwise conditions force the RCL family). It realizes the canonicality step that precedes derivation of the Recognition Composition Law.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)