Constants Alpha Genesis Curvature Jcost Verdict Genuine Cost Lt Gauss Bonnet

The curvature cost verdict

The Gauss-Bonnet theorem is a classical result in geometry: for a closed surface like a cube, the total curvature, measured by adding up the angle deficits at every vertex, always equals 4π times a whole number called the Euler characteristic. For a cube, that total is exactly 4π ≈ 12.57. This number is a topological invariant: it does not change when the surface is stretched or deformed, only when its overall shape type changes. It is a linear sum of local contributions, one from each vertex.

Recognition Science works with a different quantity, the cost, which it defines as a discrete record of the price a system pays for each recognition event. The framework's central theorem forces this cost to be a specific function, and near a stable equilibrium that function behaves quadratically: a small displacement of size ε costs about ε²/2, not a linear multiple of ε. This quadratic character matters. A linear topological invariant and a quadratic displacement cost are different kinds of objects, and one cannot be turned into the other by multiplying by a count of edges or vertices.

In Recognition Science, the framework's machine-checked library of formal theorems proves what happens when you compute the genuine quadratic cost of the cube's curvature. Each of the cube's 8 vertices has an angular deficit of π/2. Applying the quadratic cost coefficient 1/2 to each deficit and summing gives 8 · ½ · (π/2)² = π² ≈ 9.87. The theorem genuine_cost_lt_gaussBonnet proves this value is strictly less than the topological 4π. The proof is short: it rewrites the cost as π² and then uses the classical fact that π < 4.

The point of the comparison is a verdict about an earlier attempt to derive the fine-structure constant α. That attempt used a seed value 4π·11 ≈ 138.23, built by multiplying the topological 4π by an edge count of 11. The framework's library now shows this seed is a category error: it multiplies a linear topological invariant by a count and calls the product a cost, when the actual quadratic cost of the same curvature is π², an order of magnitude smaller. The seed is not a recognition cost at all, and the theorem seed_far_above_genuine_cost records that π² < 4π < 4π·11.

What the declaration does not claim is just as important. The inequality π² < 4π says nothing about the measured fine-structure constant. The genuine cost π² ≈ 9.87 is far below the measured inverse fine-structure constant 1/α ≈ 137.036, and the framework's library proves this separation explicitly. The exact value of α remains an open target, not a derived consequence. The verdict isolates the seed as the locus of the overclaim; it does not touch other forced quantities in the framework, such as the dressing function or the spectral weight, which were derived with no α input at all.

/-- The genuine quadratic J-cost `π² ≈ 9.87` is strictly below the topological
Gauss-Bonnet integral `4π ≈ 12.57`: a quadratic cost and a linear topological
invariant are different objects, and they do not even agree numerically. -/
theorem genuine_cost_lt_gaussBonnet :
    cubeCurvatureJCost < 4 * Real.pi := by
  rw [cubeCurvatureJCost_eq_pi_sq]
  nlinarith [Real.pi_pos, Real.pi_lt_four]

/-- **The genuine J-cost of the cube curvature is `π²`.** `8 · ½ · (π/2)² = π²`.
This is the honest quadratic recognition cost, contrasted with the seed's
`4π·11`. -/
theorem cubeCurvatureJCost_eq_pi_sq : cubeCurvatureJCost = Real.pi ^ 2 := by
  unfold cubeCurvatureJCost
  rw [vertex_deficit_eq, Foundation.JCostHessianC7.jcostTaylorQuadraticCoefficient_eq]
  have h8 : (cube_vertices D : ℝ) = 8 := by exact_mod_cast vertices_at_D3
  rw [h8]; ring

/-- The seed `4π·11` is far above the genuine quadratic J-cost `π²` of the cube
curvature: `π² < 4π < 4π·11`. The seed is not a recognition cost. -/
theorem seed_far_above_genuine_cost :
    cubeCurvatureJCost < Constants.alpha_seed := by
  have h1 : cubeCurvatureJCost < 4 * Real.pi := genuine_cost_lt_gaussBonnet
  have h2 : (4 : ℝ) * Real.pi < Constants.alpha_seed := by
    simp only [Constants.alpha_seed]
    nlinarith [Real.pi_pos]
  linarith

/-- The genuine quadratic J-cost is also far below the measured `α⁻¹`:
`π² < 137.030 < alphaInv`. So even the honest cost is not `α⁻¹(0)`; the cube
forces only an `O(4π)` UV-scale quantity. -/
theorem genuine_cost_far_below_alphaInv :
    cubeCurvatureJCost < Constants.alphaInv := by
  rw [cubeCurvatureJCost_eq_pi_sq]
  have h1 : Real.pi ^ 2 < 4 * Real.pi := by nlinarith [Real.pi_pos, Real.pi_lt_four]
  have h2 : (4 : ℝ) * Real.pi < 13 := by nlinarith [Real.pi_lt_d6]
  have h3 : (137.030 : ℝ) < Constants.alphaInv := Numerics.alphaInv_gt
  linarith

What this page does not claim

The theorem does not claim that π² is the measured fine-structure constant; it proves the opposite. The theorem does not claim that 4π is a recognition cost; it identifies 4π as a topological invariant. The theorem does not claim that the seed 4π·11 is a valid derivation of α; it marks the seed as a category error.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/AlphaGenesis/CurvatureJCostVerdict.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: