Gravity Analysis Regge Bloch Star Edge Origins4 D Phased Deficit Dot Edge Origin

Scaling the deficit

In the framework's analysis of gravity, a central object is the deficit phase, a number that measures how much a discrete grid of points, a ledger of events, deviates from a smooth continuous space. The declaration phasedDeficitDotEdgeOrigins_smul proves a scaling law for this quantity. It states that if you multiply the field matrix H by a constant c, the deficit phase scales by exactly that same constant. In symbols: phasedDeficitDotEdgeOrigins ty (c • H) m s t = c * phasedDeficitDotEdgeOrigins ty H m s t.

This is a homogeneity property, a standard and expected behavior for a physical quantity. It means the deficit phase behaves like a linear function of the field, not a nonlinear one. The proof is a direct computation: it unfolds the definition of the deficit phase, which is a sum over contributions from seed edges, and applies a lemma about sums of scaled terms. The theorem holds for all six hinge orbit types, all slots s and t, and any real scaling constant c.

The practical consequence is that the computation is stable under rescaling of the field. If you change the overall magnitude of H, the deficit phase adjusts proportionally, so relative comparisons between different configurations remain meaningful. This is a consistency check that the framework's construction is well-behaved, not a claim about the physical value of the deficit itself.

What the theorem does not claim is more limited than it might appear. It does not say that the deficit phase is physically meaningful or that it matches any measured gravitational quantity. It does not establish that the sum converges or that the individual contributions are finite. It does not prove that the deficit phase is invariant under any symmetry, only that it scales linearly. The theorem is a formal statement about a definition, verified by the machine-checked library, not an empirical result.

theorem phasedDeficitDotEdgeOrigins_smul (c : ℝ) (ty : HingeOrbitType)
    (H : Mat4) (m : Wave4) (s : Fin 24) (t : Fin 10) :
    phasedDeficitDotEdgeOrigins ty (c • H) m s t =
      c * phasedDeficitDotEdgeOrigins ty H m s t := by
  unfold phasedDeficitDotEdgeOrigins edgeContribPhased
  exact list_sum_map_smul_planeWave c H m (orbitCoveringPerm ty s t)
    (hingeBase s t) (seedEdgeContribs ty)

private lemma list_sum_map_smul_planeWave (c : ℝ) (H : Mat4) (m : Wave4)
    (p : Fin 24) (base : Wave4) (cs : List SeedEdgeContrib) :
    (cs.map (fun e =>
        e.weight *
          planeWaveClassPert (c • H) m
            (fun i => base i + transportOrigin p e.origin i)
            (permClass p e.cls))).sum =
      c *
        (cs.map (fun e =>
            e.weight *
              planeWaveClassPert H m
                (fun i => base i + transportOrigin p e.origin i)
                (permClass p e.cls))).sum := by
  induction cs with
  | nil => simp
  | cons hd tl ih =>
      simp only [List.map_cons, List.sum_cons]
      rw [planeWaveClassPert_smul, ih]
      ring

theorem phasedDeficitDotEdgeOrigins_smul (c : ℝ) (ty : HingeOrbitType)
    (H : Mat4) (m : Wave4) (s : Fin 24) (t : Fin 10) :
    phasedDeficitDotEdgeOrigins ty (c • H) m s t =
      c * phasedDeficitDotEdgeOrigins ty H m s t := by
  unfold phasedDeficitDotEdgeOrigins edgeContribPhased
  exact list_sum_map_smul_planeWave c H m (orbitCoveringPerm ty s t)
    (hingeBase s t) (seedEdgeContribs ty)

What this page does not claim

The deficit phase is not claimed to match any measured gravitational quantity. The theorem does not establish convergence or finiteness of the individual contributions. The deficit phase is not claimed to be invariant under any symmetry, only to scale linearly.

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/Gravity/Analysis/ReggeBlochStarEdgeOrigins4D.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: