Foundation Pair Kernel Source Coupling Named Premises Do Not Force Zero Defect

The scale freedom

In a discrete model of sources and fields, a ledger (a discrete record of events) pairs a physical source with a dual variable, like a price with a quantity. A primitive posting, the smallest indivisible unit of the ledger, fixes the integer generator of the source. But the real coordinate paired with that generator still carries an arbitrary identification scale, a freedom that a proposed law was meant to eliminate.

The theorem namedPremises_do_not_force_zeroDefect proves that a specific set of five named premises, including symmetry of the action and stationarity of the work, does not force the scale to be one. A two-site model satisfies every premise at every real coupling, yet the scale can be two, where a defect term is nonzero. The proof exhibits this counterexample directly.

This is a negative result: it closes off one route to a unique scale. The framework's library of formal theorems shows that the current package of assumptions, including the action principle and posting integrality, is insufficient to derive the proposed One-Ledger work-response law. The theorem does not say the law is false; it says these premises alone do not prove it.

The result matters because it maps the boundary of what is forced. A reader can now see that a specific, named set of principles leaves a genuine freedom, and that any future derivation of the scale must add a new ingredient beyond the current five.

/-- The current named pair-kernel premises cannot imply the zero-defect
scale-selection predicate: coupling two satisfies all of them while the
zero-defect predicate rejects it. Any positive bridge must therefore add a
genuinely scale-breaking recognition premise. -/
theorem namedPremises_do_not_force_zeroDefect :
    ¬ (∀ coupling : ℝ,
      NamedPremises coupling →
        ZeroDefectDualIdentification coupling) := by
  intro hforce
  exact zeroDefectDualIdentification_excludes_two
    (hforce 2 (namedPremises_all_couplings 2))

theorem namedPremises_all_couplings
    (coupling : ℝ) : NamedPremises coupling where
  primitive_generator := primitivePosting_isPrimitive
  action_symmetric := twoSiteWeight_symmetric
  posting_antisymmetric := elementaryPosting_antisymmetric (0 : Fin 2) 1
  posting_is_unit_source := elementaryPosting_divergence_eq_dipole (0 : Fin 2) 1
  work_stationary := twoSite_stationary_at_every_coefficient coupling

/-- The live normalization decoy at scale two is rejected if, and only if,
the zero-defect identification law is supplied. -/
theorem zeroDefectDualIdentification_excludes_two :
    ¬ ZeroDefectDualIdentification 2 := by
  rw [zeroDefectDualIdentification_iff_one]
  norm_num

What this page does not claim

The theorem does not claim the One-Ledger law is false, only that these premises do not derive it. The theorem does not claim the scale freedom exists in all possible models, only in the two-site counterexample. The theorem does not claim the named premises are the only possible set of physical assumptions.

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/PairKernelSourceCoupling.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: