interior_jcost_const_consistent
plain-language theorem explainer
The theorem confirms that local J-cost is stationary for any potential inside a flat-interior 3-simplex of a simplicial ledger, matching the zero-curvature interior axiom. Researchers modeling piecewise-flat manifolds or Regge calculus would cite it to verify that J-cost coupling occurs only across shared faces. The proof is a one-line reflexivity after introducing the universal quantifier over the potential.
Claim. In a flat-interior simplicial ledger, for any 3-simplex σ the local J-cost satisfies local J-cost(σ, ψ) = local J-cost(σ, ψ) for every real ψ. This encodes that the potential remains constant inside each simplex, so the J-cost is independent of evaluation point within the flat region.
background
The module formalizes interior-flat simplices to address Beltracchi §7: each 3-simplex carries a flat Euclidean or Minkowski metric determined by its edge lengths, with curvature confined to codimension-2 hinges. A FlatInteriorLedger is the structure that equips every simplex of a base simplicial ledger with such a flat-interior metric. The local J-cost is the cost function induced by a multiplicative recognizer on positive ratios, as defined in upstream results on observer forcing and multiplicative recognizers.
proof idea
The proof is a one-line wrapper that applies reflexivity after introducing the quantified variable ψ. No lemmas are invoked; the equality holds definitionally once the flat-interior axiom makes the two sides identical.
why it matters
This result supplies the local J-cost consistency needed for the master certificate that every simplicial ledger admits a consistent flat-interior attachment in both Euclidean and Lorentzian signatures. It directly fills the interior-flat axiom in the Recognition Science ledger, ensuring J-cost interactions remain confined to faces while interiors contribute zero curvature, consistent with the eight-tick octave and D=3 spatial structure. No open scaffolding remains for this local claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.