Pith. sign in
module module high

IndisputableMonolith.Foundation.DAlembert.TriangulatedProof

show as:
view Lean formalization →

The module proves the fundamental trichotomy for cost functions under structural axioms in Recognition Science: exactly one of the hyperbolic J-cost branch, the flat quadratic branch, or the entangling interaction branch holds. Foundation researchers closing d'Alembert inevitability arguments cite this result. The argument triangulates the three gates via case analysis on the imported necessity and characterization modules.

claimUnder the structural axioms of symmetry, normalization, $C^2$ smoothness, calibration, and existence of a combiner $P$, exactly one of the following holds: the cost metric has constant nonzero curvature (hyperbolic branch with $G''(t) = G(t) + 1$), the combiner is additive (flat branch with $P(u,v) = 2u + 2v$), or the cross-derivative satisfies $\partial^2 P / \partial u \partial v \neq 0$ (entanglement branch).

background

This module operates in the d'Alembert setting for the log-lift of the cost function $F$. The upstream Counterexamples module documents that the mere existence of some combiner $P$ satisfying $F(xy) + F(x/y) = P(F(x), F(y))$ does not force the d'Alembert structure for the log-lift of $F$. NecessityGates adds the requirements of symmetry, normalization, $C^2$, and calibration.

The EntanglementGate requires that the combiner $P$ has nonzero cross-derivative $\partial^2 P / \partial u \partial v$, ruling out the additive case. The CurvatureGate requires that the cost metric has constant nonzero curvature, expressed via $G(t) = F(e^t)$ with $ds^2 = G''(t) dt^2$. The FourthGate formalizes the d'Alembert structure condition, while Unconditional provides the base case.

proof idea

The module structures its argument as a triangulation of the three gates. It imports the counterexample to show the need for gates, then uses the necessity gates and the specific characterizations from EntanglementGate, CurvatureGate, and FourthGate to prove that the branches are mutually exclusive and exhaustive under the axioms. The main result combines these into the trichotomy via case analysis on the imported modules.

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, which identifies the choke points where degrees of freedom are relocated in the move from MP to CPM foundations. It completes the necessity argument for the d'Alembert/RCL structure in the Recognition Science framework.

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)