pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.TriangulatedProof

show as:
view Lean formalization →

The module establishes the fundamental trichotomy for the cost function under structural axioms of symmetry, normalization, C2 smoothness and calibration: exactly one branch holds. Researchers deriving inevitability of the Recognition Composition Law cite this result to close the gap left by generic combiners. The argument assembles the curvature, entanglement and d'Alembert gates with counterexamples to force the case split.

claimUnder symmetry, normalization, $C^2$ smoothness and calibration, exactly one of the following holds for the cost $F$: the hyperbolic branch ($G''(t)=G(t)+1$), the flat branch, or the branch in which the combiner forces nonzero cross-derivative entanglement.

background

The module sits inside the d'Alembert analysis of the cost function in Recognition Science. The Curvature Gate requires constant nonzero curvature via the log-coordinate metric $ds^2 = G''(t) dt^2$. The Entanglement Gate requires nonzero cross-derivative in the combiner $P$. The Fourth Gate enforces the d'Alembert structure. NecessityGates records that symmetry plus normalization plus $C^2$ plus calibration plus existence of some combiner $P$ does not force the d'Alembert or RCL structure.

proof idea

The module imports the counterexamples, necessity gates, curvature gate, entanglement gate, fourth gate and unconditional modules, then structures the argument as a case analysis across the three branches to reach the triangulated inevitability statement.

why it matters in Recognition Science

This module supplies the triangulated proof that feeds the InevitabilityEquivalence module (bridging abstract inevitability claims to concrete CPM/cost definitions) and the InevitabilityStructure module (formalizing choke points). It completes the step from the necessity gates to full inevitability of the RCL under the structural axioms.

scope and limits

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (16)