pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.TriangulatedProof

show as:
view Lean formalization →

The module establishes the fundamental trichotomy for cost functions: under symmetry, normalization, C² regularity and existence of a combiner P, exactly one of the hyperbolic J-cost branch, flat F-quad branch or entangling RCL branch holds. Researchers formalizing d'Alembert inevitability from the Recognition Composition Law would cite it to close the necessity argument. The module assembles the curvature, entanglement and fourth gates with counterexamples into one triangulated structure that rules out mixed cases.

claimUnder symmetry, normalization, $C^2$ regularity and existence of a combiner $P$ satisfying $F(xy)+F(x/y)=P(F(x),F(y))$, exactly one of the following holds: the $J$-cost is hyperbolic ($G''(t)=G(t)+1$), the $F$-quad is flat, or the combiner has nonzero cross-derivative $P_{uv}≠0$.

background

The module resides in the Foundation.DAlembert namespace and imports Cost together with the four gate modules and Counterexamples. It rests on the fact, documented in Counterexamples, that (symmetry + normalization + C² + calibration + existence of some combiner P) does not force the d'Alembert structure for the log-lift of F. CurvatureGate requires constant nonzero curvature of the metric ds² = G''(t) dt² on the log-coordinate G(t) = F(e^t). EntanglementGate requires nonzero cross-derivative ∂²P/∂u∂v. FourthGate encodes the d'Alembert ODE closure.

proof idea

The module organizes the argument by defining the three mutually exclusive branches (CostBranch, Jcost_is_hyperbolic, Fquad_is_flat, RCL_is_entangling) and proving full_inevitability_triangulated. It sequences the necessity lemmas from NecessityGates, applies the curvature and entanglement characterizations, invokes the counterexamples to exclude the additive case, and closes with the unconditional gate to obtain the trichotomy.

why it matters in Recognition Science

This module supplies the concrete trichotomy that feeds InevitabilityEquivalence and InevitabilityStructure. It converts the abstract inevitability claim into a statement about CPM/cost definitions by showing how the three gates together force exactly one branch, thereby closing the necessity argument for the Recognition Composition Law inside the Foundation layer.

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)