totalCost
plain-language theorem explainer
The total cost functional sums the normalized bit cost of a single recognition event with the quadratic curvature cost at scale λ. Researchers deriving the recognition length λ_rec non-circularly from bit and curvature contributions cite this when balancing ledger costs to obtain the optimal scale. It is realized as the direct sum of the constant 1 and the term 2λ².
Claim. The total cost functional is defined by $C(λ) = 1 + 2λ²$, where the constant 1 is the normalized bit cost of one recognition event and $2λ²$ is the curvature cost obtained from Gauss-Bonnet normalization on $S²$ with Euler characteristic 2 and four curvature quanta distributed over the vertices of $Q_3$.
background
The Lambda_rec Derivation module formalizes a non-circular derivation of the recognition length λ_rec. It combines a fixed bit cost with a scale-dependent curvature cost and defines Newton's constant G afterward as $G := π λ_rec² c³ / ℏ$. The bit cost equals 1 by normalization for a single recognition event. The curvature cost equals $2λ²$, obtained by distributing four curvature quanta over the eight vertices of $Q_3$, applying Gauss-Bonnet normalization on $S²$ with χ = 2, and using bounding area $4πλ²$.
proof idea
The definition is a one-line wrapper that adds the constant bit cost to the curvature cost evaluated at λ. It composes the upstream definitions of the normalized bit cost and the curvature cost without further lemmas or tactics.
why it matters
This supplies the cost functional used to derive λ_rec and G. It is invoked by costDensity and isBalanced in the DarkEnergy module to enforce ledger balance in spacetime regions, and by SMLagrangianCert to certify vacuum properties. It realizes the curvature-extremum step in the non-circular derivation of constants, consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.