Foundation Pair Kernel Bounded Coupling Bounded Coupling Season Status

The season's verdict

The declaration boundedCoupling_season_status is a status report from a machine-checked library of formal theorems. It bundles three results about recognition, the framework's term for a discrete record of events and the relations between them. The first result is a closed negative: the bare assumptions of a recognition structure and an atomic tick, the smallest unit of recognition, do not force the coupling between events to be bounded in range. The result exhibits a concrete carrier where the recognition relation is the all-true relation, the mean-field weight graph is supported, and yet boundedness and finite range both fail. This is not a gap in the proof; it is a proved statement that the basic assumptions alone are insufficient.

The second and third results concern a specific three-dimensional lattice geometry, the Door-2 carrier. Here the framework proves that the box weight, a particular weight assignment, is finite-range when measured in the encoded ℓ¹ distance on the lattice. The recognition relation is the nearest-neighbor relation, and the result shows that nonzero box weights force the finite-range property at radius 1. In contrast, the mean-field weight fails this same finite-range predicate on the same geometry. The status theorem combines these three facts into one statement: the basic assumptions fail to force bounded coupling, the box weight satisfies it on the lattice, and the mean-field weight does not.

What the declaration does not claim is as important as what it proves. It does not prove that bounded coupling is forced by the recognition framework alone; the closed negative explicitly rules that out. It does not establish that the three-dimensional lattice geometry is itself derived from deeper principles. The lattice recognition structure is a definitional choice, not a forced consequence, and the result tags it as a model. The remaining premise, named ProductionLatticeCouplingObligation, is a hypothesis: that production pair weights can be forced onto a metric-bounded recognition relation equivalent to the lattice geometry. Until that premise is derived, the global finite-range statement in the original one-dimensional form remains open.

The practical consequence is a precise map of what is settled and what is not. The framework has a theorem-grade export for the three-dimensional lattice path, and a proved obstruction for the bare assumptions. The next step is not to patch the obstruction but to derive the missing premise from deeper recognition dynamics. That is the named target, and the status theorem makes the boundary explicit.

/-- **THEOREM (closed negative).** Bare `RecognitionStructure` (via
`tickCarrier`, whose `R` is all-true) plus a valid `AtomicTick` coexist with
mean-field weights that fail both `BoundedRecognitionRelation` and
`FiniteRange`. This is the Lean form of the season-1 obstruction. -/
theorem recognitionStructure_atomicTick_do_not_force_boundedCoupling
    (radius : ℕ) :
    ∃ n : ℕ,
      Nonempty (AtomicTick (tickCarrier n)) ∧
        ¬ BoundedRecognitionRelation (tickCarrier n).R radius ∧
          RelationSupportsWeight (tickCarrier n).R (meanFieldWeight n) ∧
            ¬ FiniteRange (meanFieldWeight n) radius := by
  refine ⟨radius + 2, ⟨scheduleAtomicTick (fun _ => ⟨0, by omega⟩)⟩, ?_,
    meanFieldWeight_supported_on_unconstrained (radius + 2),
    meanFieldWeight_not_finiteRange radius (radius + 2) (le_refl _)⟩
  intro hB
  have hi : (0 : ℕ) < radius + 2 := Nat.succ_pos _
  have hj : radius + 1 < radius + 2 := Nat.lt_succ_self _
  have hle :
      cellDist (⟨0, hi⟩ : Fin (radius + 2)) ⟨radius + 1, hj⟩ ≤ radius :=
    hB ⟨0, hi⟩ ⟨radius + 1, hj⟩ trivial
  have hdist :
      cellDist (⟨0, hi⟩ : Fin (radius + 2)) ⟨radius + 1, hj⟩ = radius + 1 := by
    simp only [cellDist, Nat.dist]
    omega
  omega

/-- Direct form: `boxWeight` is finite-range in the encoded ℓ¹ metric. -/
theorem boxWeight_finiteRangeOn (L : ℕ) :
    FiniteRangeOn (boxWeight L) (encodedDist3 L) 1 :=
  (boxWeight_finiteRangeOn_export_v1 L).2.2

theorem meanFieldWeight_not_finiteRangeOn_encodedDist3
    (L : ℕ) (hL : 2 ≤ L) :
    ¬ FiniteRangeOn (meanFieldWeight (L * L * L)) (encodedDist3 L) 1 := by
  intro hFR
  -- Two axis steps (still available at L = 2) give encodedDist3 = 2 > 1.
  set o : Site3 L := ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)
  set e : Site3 L := ((⟨1, by omega⟩, ⟨1, by omega⟩), ⟨0, by omega⟩)
  have hdist : encodedDist3 L (enc3 L o) (enc3 L e) = 2 := by
    simp [encodedDist3, Equiv.symm_apply_apply, dist3, Nat.dist, o, e]
  have hfar : 1 < encodedDist3 L (enc3 L o) (enc3 L e) := by
    rw [hdist]
    norm_num
  have hz := hFR (enc3 L o) (enc3 L e) hfar
  simp only [meanFieldWeight] at hz
  exact one_ne_zero hz

/-- Strengthened recognition structure for the Door-2 D=3 carrier.
This commits `R` to the ℓ¹ unit ball. It is NOT derived from bare
`RecognitionStructure`; forcing that commitment is
`ProductionLatticeCouplingObligation`. -/
def lattice3RecognitionStructure (L : ℕ) : RecognitionStructure where
  U := Fin (L * L * L)
  R := lattice3RecognitionRelation L

/-- Remaining production premise after the metric export is banked.
Force (from deeper Recognition dynamics) or commit that production pair
weights are supported on a metric-bounded recognition relation equivalent
to the Door-2 D=3 NN lattice geometry (`lattice3RecognitionStructure`).
Until then, the global 1D `FiniteRange` hypothesis stays open; the D=3
path has a THEOREM-grade `FiniteRangeOn` inhabitant. -/
def ProductionLatticeCouplingObligation : String :=
  "Force production WeightedLedgerGraph support onto a metric-bounded \
recognition relation equivalent to PairKernelLattice3 / \
lattice3RecognitionStructure (dist3 ≤ 1), or derive that commitment from \
Recognition dynamics beyond bare RecognitionStructure + AtomicTick."

What this page does not claim

Bounded coupling is forced by the recognition framework alone. The three-dimensional lattice geometry is derived from deeper principles; it is a committed model. The global one-dimensional finite-range statement is proved; it remains a hypothesis.

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/Foundation/PairKernelBoundedCoupling.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: