Gravity Seven Gaps Zq Phase Structure Phased Zq Pairing Witness

The pairing witness

In the Recognition Science framework's account of gravity, a central object is a path sum over triangulations of space, a discrete sum of complex weights. A naive bound on the size of this sum is the total mass of all configurations, a number that can be large. The declaration phased_Zq_pairing_witness establishes a concrete, machine-checked example where this bound is improved: for a specific choice of phases, the sum's magnitude is at most the total mass minus 2, a strictly better bound than the naive one.

The mechanism is pairing. The proof exhibits two distinct classes of triangulations, the empty complex and the one-point complex, and assigns them opposite phases: 0 and π. Because these phases differ by π, their contributions to the sum cancel exactly. The theorem shows this cancellation is not a formal possibility but a realized one, by explicitly discharging all the hypotheses needed for the cancellation to occur. The result is a strict inequality, ‖Zq‖ < totalClassMass, which beats the triangle inequality.

The witness is a theorem, not a model. It is proved in the machine-checked library with no unproven assumptions. However, its scope is narrow. It applies only at a fixed complexity cap, B = 2, meaning the sum includes only triangulations with at most two vertices. This is not a limit, and it is not a proof of the continuum limit. The declaration also does not provide a physical mechanism for choosing the phases; the phase model is supplied by hand, not derived from the framework's principles.

What the witness changes is the status of a research question. It proves that the cancellation mechanism is satisfiable, that the pairing hypotheses are not vacuous. This turns the question of whether such cancellations can improve the path sum from a matter of speculation into a matter of finding the right phase model, a task that remains open.

/-- **HEADLINE (non-vacuous quantitative cancellation witness).**  The
explicit phase model at `B = 2` beats the triangle bound by EXACTLY the
paired mass 2: `‖Zq‖ <= totalClassMass 2 - 2`.  This discharges the
pairing hypotheses of the general theorems in one concrete instance. -/
theorem phased_Zq_pairing_witness :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 := by
  have hb := Zq_pairing_bound 2 (phasedWeight witnessPhaseModel)
    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
    witnessPairing_cancel
  rw [witnessPaired_mass] at hb
  exact hb

/-- **HEADLINE (strict improvement, witnessed).**  The phased `Zq` of the
explicit witness model is STRICTLY below the triangle bound.  Genuine
cancellation, not an inequality-shuffling tautology: the bound drop is
the exact paired mass. -/
theorem phased_Zq_beats_triangle_witness :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ < totalClassMass 2 :=
  Zq_pairing_beats_triangle 2 (phasedWeight witnessPhaseModel)
    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
    witnessPairing_cancel ⟨emptyClass, Finset.mem_singleton_self _⟩

/-- **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 declaration does not prove the continuum limit of the phased path sum. It does not derive the phase model from a physical principle. It does not claim that pairings exist for every phase model or every complexity cap.

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: