Gravity Seven Gaps Zq Phase Structure Zq Phase Structure Status Grounded

Phase structure status

In quantum gravity, a path sum adds complex weights over many geometric configurations. The sum is often infinite or ill-defined, so one tries to tame it. The Recognition Science framework's library, a machine-checked collection of formal theorems, studies a path sum over triangulations, discrete pieces of space built from vertices, edges, and tetrahedra. The declaration zqPhaseStructureStatus_grounded is a compact status report: a record of which structural properties of that path sum have been proved, which have been modeled by choice, and which remain open.

The record first confirms that the path sum is well behaved at any fixed complexity cap, a bound on the number of vertices. For any choice of oscillatory phase, a real number attached to each labeled configuration, the sum is finite and its magnitude is bounded by the total mass of all configurations, which in turn is at most the number of distinct triangulation classes. This is a theorem: Zq_phased_wellDefined proves the bound for every phase model.

The deeper result is conditional cancellation. If one can injectively pair some configurations with others whose contributions are exactly opposite, then the paired terms cancel completely, and the magnitude bound improves strictly below the triangle inequality. The general theorem Zq_pairing_beats_triangle proves this improvement under the explicit pairing hypothesis. The library also proves that two equal masses with phases differing by π cancel exactly. To show the hypothesis is not empty, it exhibits a concrete phase model at cap 2: phase 0 on the empty complex, phase π on the one-point complex. For that model, the pairing is discharged concretely, and the chain phased_Zq_witness_chain proves the improved bound is nonnegative and strictly better than the triangle bound.

What the status record explicitly does not claim matters as much. The continuum limit of the phased path sum is open, and the complexity cap is not a mesh refinement. Regulator removal, the procedure that would make the sum well defined in the limit, is not derived for any oscillatory phase; a separate theorem states that the zero-phase route is dead. The phase function itself is a model, a definitional choice, not derived from a substrate. The record zqPhaseStructureStatus sets all three flags, Z_RS_continuum_limit, oscillatory_regulator_removal_derived, and substrate_phase_derived, to false.

The practical upshot: the framework has proved a finite, machine-checked cancellation mechanism that improves bounds at fixed cap, and it has shown by example that the mechanism is satisfiable. The step from that finite structure to a continuum theory remains a target, not a result.

/-- **THEOREM (well-definedness of the phased Zq at fixed cap).**  For
every phase model, the phased quotient-first path sum has unit-modulus
weights and satisfies the proved finiteness bounds.  This is a structure
theorem at fixed complexity cap, NOT a continuum-limit statement. -/
theorem Zq_phased_wellDefined (B : ℕ) (P : PhaseModel B) :
    (∀ q, ‖phasedWeight P q‖ = 1) ∧
    ‖Zq B (phasedWeight P)‖ ≤ totalClassMass B ∧
    ‖Zq B (phasedWeight P)‖ ≤ (Fintype.card (TriangulationClass B) : ℝ) := by
  have hb := Zq_norm_le_totalClassMass B (phasedWeight P)
    (fun q => le_of_eq (phasedWeight_norm P q))
  exact ⟨phasedWeight_norm P, hb, le_trans hb (totalClassMass_le_card B)⟩

/-- **THEOREM (strictly better than the triangle inequality).**  Under the
pairing hypothesis with a NONEMPTY paired family, the phased `Zq` is
STRICTLY below the triangle bound `totalClassMass`. -/
theorem Zq_pairing_beats_triangle (B : ℕ) (wq : TriangulationClass B → ℂ)
    (hw : ∀ q, ‖wq q‖ ≤ 1)
    (s : Finset (TriangulationClass B))
    (j : TriangulationClass B → TriangulationClass B)
    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
    (hdisj : ∀ q ∈ s, j q ∉ s)
    (hcancel : ∀ q ∈ s,
      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
        = -((mu (Quotient.out q) : ℂ) * wq q))
    (hne : s.Nonempty) :
    ‖Zq B wq‖ < totalClassMass B := by
  have hb := Zq_pairing_bound B wq hw s j hinj hdisj hcancel
  have hpos : 0 < ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) := by
    obtain ⟨q0, hq0⟩ := hne
    exact Finset.sum_pos (fun q _ => mu_pos _)
      ⟨q0, Finset.mem_union_left _ hq0⟩
  linarith

/-- **THEOREM (two-term exact cancellation).**  Equal masses at phases
`θ` and `θ + π` cancel exactly. -/
theorem opposite_phase_pair_cancels (m θ : ℝ) :
    (m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))
      + (m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ)) = 0 := by
  rw [opposite_phase_exp, mul_neg, add_neg_cancel]

/-- **HEADLINE (single-theorem chain).**  The full advertised chain in one
kernel statement: the witness `Zq` is bounded by `totalClassMass 2 - 2`,
that improved bound is strictly below the triangle bound, and it is
nonnegative. -/
theorem phased_Zq_witness_chain :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 ∧
    totalClassMass 2 - 2 < totalClassMass 2 ∧
    (0 : ℝ) ≤ totalClassMass 2 - 2 :=
  ⟨phased_Zq_pairing_witness, by linarith,
    by linarith [two_le_totalClassMass_two]⟩

What this page does not claim

The continuum limit of the phased path sum is not proved. Regulator removal is not derived for any oscillatory phase. The phase function is a definitional model, not a derived quantity.

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/SevenGaps/ZqPhaseStructure.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: