CostBranch
plain-language theorem explainer
CostBranch enumerates the two admissible forms of the cost functional under the structural axioms of Recognition Science: the flat quadratic branch with additive propagation and the hyperbolic branch with J-cost and RCL interaction. Researchers working on the d'Alembert triangulated proof or the four-gate inevitability argument cite this case split to organize the exclusion of alternatives. The declaration is a direct inductive definition that supplies the exhaustive dichotomy for downstream case analysis.
Claim. The cost functional belongs to one of two branches: the flat branch where the reparametrized cost satisfies $G(t)=t^2/2$ with additive propagation, or the hyperbolic branch where $G(t)=cosh(t)-1$ with propagation obeying the recognition composition law.
background
The TriangulatedProof module assembles four gates that together force the cost functional into a unique form. Gate 1 (interaction) distinguishes additive from entangling propagators; Gate 2 (entanglement) checks the mixed second difference; Gate 3 (curvature) imposes the hyperbolic ODE $G''=G+1$; Gate 4 (d'Alembert) requires the functional equation $H(t+u)+H(t-u)=2H(t)H(u)$ for $H=G+1$. The inductive CostBranch supplies the exhaustive case distinction between the quadratic example Fquad (flat, no interaction) and the J-cost example (hyperbolic, RCL interaction). Upstream results include the Gate structure from CircuitLedger, which enforces locality of at most two parents, and the reparametrization G from Cost.FunctionalEquation that converts the original F into a function of log-coordinate t.
proof idea
The declaration is an inductive definition with two constructors. The flat constructor is annotated with the quadratic Gquad example; the hyperbolic constructor is annotated with the cosh-1 form and RCL. No tactics or lemmas are invoked; the definition itself provides the exhaustive dichotomy used by later theorems in the same module.
why it matters
CostBranch supplies the case split required by the four-gate argument that culminates in full_inevitability_triangulated. It directly encodes the trichotomy claim stated in the module header and links the interaction gate (NecessityGates) to the curvature and d'Alembert gates. Within the Recognition Science framework it corresponds to the T5 J-uniqueness step and the subsequent forcing of the hyperbolic solution once interaction is present. The definition closes the structural alternatives before the unconditional derivation of P=RCL in the Unconditional sibling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.