CalibratedAgainstGraph
A deficit angle functional D is calibrated against a weighted ledger graph G when the Regge sum of D on the conformal edge-length field equals the jcost-to-Regge factor times the Laplacian action of G for every log-potential ε. Researchers proving the simplicial form of the field-curvature identity cite this equational condition as the general discharge hypothesis. The definition is a direct renaming of the linearization hypothesis with no proof obligations.
claimLet $D$ be a deficit angle functional, $a>0$ a scale, hinges a list of hinge data, and $G$ a weighted ledger graph. Then $D$ is calibrated against $G$ when, for every log-potential $ε$, the Regge sum of $D$ evaluated on the conformal edge-length field at scale $a$ equals $κ$ times the Laplacian action of $G$ on $ε$, where $κ$ denotes the jcost-to-Regge conversion factor.
background
This definition sits in the SimplicialDeficitDischarge module, Phase C5 of the program to realize Theorem 5.1 (field-curvature identity) as a Lean theorem. It composes Phases C1–C4 by requiring that any pre-calibrated DeficitAngleFunctional matches the J-cost Dirichlet energy on the ledger graph via the per-hinge identity $A_h · δ_h = (κ/2) · G.weight · (ε_i − ε_j)^2$ under the conformal identification of hinges and edges.
proof idea
The definition is a direct equational statement. It serves as a one-line wrapper that renames ReggeDeficitLinearizationHypothesis for clarity in the simplicial setting, with the body simply asserting the forall equality between regge_sum and the scaled laplacian_action.
why it matters in Recognition Science
CalibratedAgainstGraph supplies the hypothesis for the parent theorems field_curvature_identity_simplicial and field_curvature_identity_simplicial_einstein, which state that the J-cost energy equals (1/κ) times the Regge action on the conformal field. It fills the general simplicial case of paper Theorem 5.1, extending the cubic lattice result from Phase A and the linear_regge_vanishes guarantee from Phase C4. It touches the open question of explicit calibration constructions for arbitrary simplicial complexes.
scope and limits
- Does not construct an explicit DeficitAngleFunctional for a given ledger graph.
- Does not verify the equality outside the conformal ε-field.
- Does not address higher-order curvature corrections.
- Does not prove existence of calibrations beyond the cubic and linear cases.
Lean usage
theorem discharge_from_calib {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a) (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) (hCal : CalibratedAgainstGraph D a ha hinges G) : ReggeDeficitLinearizationHypothesis D a ha hinges G := (calibrated_iff_hypothesis D a ha hinges G).mp hCalformal statement (Lean)
80def CalibratedAgainstGraph {n : ℕ}
81 (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
82 (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
proof body
Definition body.
83 ∀ ε : LogPotential n,
84 regge_sum D (conformal_edge_length_field a ha ε) hinges
85 = jcost_to_regge_factor * laplacian_action G ε
86
87/-- Trivial observation: `CalibratedAgainstGraph` and
88 `ReggeDeficitLinearizationHypothesis` are definitionally the same
89 statement. The rename clarifies that the matching is a *property*
90 of the functional, not a result of the linearization per se. -/