pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.TriangulatedProof

show as:
view Lean formalization →

The TriangulatedProof module establishes the fundamental trichotomy under Recognition Science structural axioms: exactly one branch holds among the J-cost hyperbolic, F-quad flat, and RCL entangling paths. Researchers formalizing inevitability of the d'Alembert equation in cost functions cite it to close the necessity argument. The module triangulates by importing the gate modules, counterexamples, and unconditional results to prove the exhaustive case split.

claimUnder the structural axioms (symmetry, normalization, $C^2$, calibration), exactly one of the following holds: the J-cost function is hyperbolic, the F-quad function is flat, or the RCL combiner is entangling.

background

This module sits inside the d'Alembert development and imports Cost together with the four gate modules and the counterexamples. The Counterexamples module records that existence of some combiner $P$ satisfying $F(xy)+F(x/y)=P(F(x),F(y))$ does not force the d'Alembert structure on the log-lift. NecessityGates shows that symmetry plus normalization plus $C^2$ plus calibration plus some $P$ still fails to force the structure. CurvatureGate requires the cost metric to have constant nonzero curvature via $G''(t)=G(t)+1$ in log coordinates. EntanglementGate requires the combiner $P$ to have nonzero cross-derivative. FourthGate encodes the d'Alembert functional equation itself.

proof idea

The module is organized as a triangulation: it imports the gate modules and counterexamples, then proves the sibling theorems (CostBranch, Jcost_is_hyperbolic, Fquad_is_flat, RCL_is_entangling, additive_not_entangling, interaction_forces_entanglement, and full_inevitability_triangulated) that establish the three mutually exclusive branches and their exhaustive coverage under the axioms.

why it matters in Recognition Science

The module supplies the concrete trichotomy that feeds InevitabilityEquivalence (bridging abstract inevitability claims to concrete CPM/cost definitions) and InevitabilityStructure (relocating degrees of freedom from MP to CPM foundations). It closes the gap left by the necessity gates and counterexamples, confirming that the structural axioms plus the three gates force exactly one branch and thereby the d'Alembert/RCL outcome.

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)