Verification Zmap Constraint Pass2

A forced polynomial

The module called verification zmap constraint pass2 is a step in the Recognition Science framework's program of deriving particle properties from a discrete ledger, a record of recognition events. It works with a polynomial of the form Z = c + a·Q̃² + b·Q̃⁴, where Q̃ is a charge-like variable and a, b, c are coefficients. The question is whether those coefficients are arbitrary or forced by data.

The module uses two quark family targets: an up-type value Z_u = 276 at Q̃ = 4, and a down-type value Z_d = 24 at Q̃ = -2. It also assumes two structural constraints: the quadratic weight a is nonnegative, and the quartic term is present, meaning b is positive. Under these conditions, a machine-checked theorem proves that the coefficients are uniquely a = 1, b = 1, c = 4. The proof is in the framework's machine-checked library of formal theorems, and it runs by direct computation once the assumptions are stated.

With those coefficients fixed, the module checks two consequences. The quark values at the given points reproduce the anchors exactly: Z(4) = 276 and Z(-2) = 24. And for a lepton offset c = 0, the value at Q̃ = -6 is fixed to 1332. These are not new measurements; they are consistency checks showing that the forced polynomial agrees with the targets it was built from.

In plain language, this pass removes a large part of coefficient arbitrariness. Before it, the polynomial could have many shapes; after it, only one shape is possible given the two data points and the mild structural assumptions. The module does not yet derive the polynomial from first principles of recognition topology, but it narrows the space of possibilities sharply, which is a necessary step toward that larger goal.

/-- Quark constraints force `(a,b,c) = (1,1,4)` under mild structural assumptions. -/
theorem quark_constraints_force_coeffs
    {c a b : ℤ}
    (h_up   : Zpoly c a b 4    = 276)
    (h_down : Zpoly c a b (-2) = 24)
    (ha_nonneg : 0 ≤ a)
    (hb_pos : 0 < b) :
    a = 1 ∧ b = 1 ∧ c = 4 := by
  have hup : c + 16 * a + 256 * b = 276 := by
    simpa [Zpoly, mul_comm, mul_left_comm, mul_assoc, add_comm, add_left_comm, add_assoc]
      using h_up
  have hdown : c + 4 * a + 16 * b = 24 := by
    simpa [Zpoly, mul_comm, mul_left_comm, mul_assoc, add_comm, add_left_comm, add_assoc]
      using h_down
  have hrel : a + 20 * b = 21 := by
    linarith [hup, hdown]
  have hb_one : b = 1 := by
    omega
  have ha_one : a = 1 := by
    omega
  have hc_four : c = 4 := by
    linarith [hdown, ha_one, hb_one]
  exact ⟨ha_one, hb_one, hc_four⟩

/-- Quark values with forced coefficients are exactly the two family anchors. -/
theorem quark_values_with_forced_coeffs :
    Zpoly 4 1 1 4 = 276 ∧ Zpoly 4 1 1 (-2) = 24 := by
  constructor <;> norm_num [Zpoly]

/-- With the forced coefficients and lepton offset `c = 0`, the lepton value is fixed. -/
theorem lepton_value_with_forced_coeffs :
    Zpoly 0 1 1 (-6) = 1332 := by
  norm_num [Zpoly]

What this page does not claim

This module does not derive the Z-map polynomial from first principles of recognition topology. The lepton value 1332 is a consistency check, not a new measurement or prediction. The structural assumptions a ≥ 0 and b > 0 are inputs, not themselves derived here.

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/Verification/ZMapConstraintPass2.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: