Foundation Pair Kernel Physical Source Law One Act Physical Dual Forces Scale On

The one-act dual lock

In the Recognition Science framework, a ledger is a discrete record of recognition events, and the framework models physical sources as entries in that record. The declaration oneActPhysicalDual_forces_scale_one proves a specific constraint: if you have a one-act physical dual event, meaning a single measurement using an instrument whose readout is determined by a curvature law, then the scale of that event must be exactly 1. The proof is short: the instrument's unit is forced to be canonical (equal to 1), and the instrument reads the scale, so the scale is 1.

This result is one of two candidate laws for fixing the absolute source scale in the framework. The other candidate, called the native action-quantum reciprocal, instead sets the source magnitude to the reciprocal of the pi-free native action quantum, which is the golden ratio raised to the fifth power, about 11.09. The two candidates select distinct magnitudes: 1 versus about 11.09. The theorem oneActPhysicalDual_forces_scale_one is what makes the first candidate work: it rejects scale 2 by continuity of the curvature function, not by applying a defect law to a free coordinate.

The framework's library also proves that the named premises alone do not force either candidate. There is a theorem showing that the named premises do not imply the existence of a one-act physical dual event at every scale. Another theorem shows they do not imply the native quantum source law. So the one-act dual lock is an additional hypothesis, not a consequence of the base premises. The framework tags the reachability of a unique banked source magnitude as HYPOTHESIS, meaning it predicts this but has not yet derived it.

What the declaration does not claim: it does not claim that the one-act dual is the only way to fix the scale, and it does not claim that the physical bridge from recognition events to actual particles is complete. That bridge remains open. The theorem is a precise statement about a mathematical model, not a direct measurement of nature.

theorem oneActPhysicalDual_forces_scale_one
    (E : OneActDualEvent) (_hE : IsOneActPhysicalDual E) :
    E.scale = 1 := by
  have hunit : E.instrument.unit = 1 :=
    instrument_forces_canonical_unit E.instrument
  exact E.instrument_reads_scale.symm.trans hunit

/-- The two candidates select different magnitudes. -/
theorem candidates_select_distinct_magnitudes :
    candidateA_sourceMagnitudeExpr.eval ≠
      candidateB_sourceMagnitudeExpr.eval := by
  rw [candidateA_sourceMagnitude_eq_one]
  change (1 : ℝ) ≠ nativeActionQuantumInv
  rw [nativeActionQuantumInv_eq_phi_pow_five]
  exact ne_of_lt goldenRatio_pow_five_gt_one

/-- Named premises do not construct a one-act dual lock: coupling `2`
satisfies every named premise while Candidate A rejects scale `2`. -/
theorem namedPremises_do_not_force_oneActPhysicalDual :
    ¬ (∀ coupling : ℝ,
      NamedPremises coupling →
        ∃ E : OneActDualEvent,
          E.scale = coupling ∧ IsOneActPhysicalDual E) := by
  intro hforce
  obtain ⟨E, hscale, hE⟩ := hforce 2 (namedPremises_all_couplings 2)
  exact oneActPhysicalDual_rejects_two E hE hscale

/-- Named premises do not force Candidate B. -/
theorem namedPremises_do_not_force_nativeQuantumSourceLaw :
    ¬ (∀ coupling : ℝ,
      NamedPremises coupling → NativeQuantumSourceLaw coupling) := by
  intro hforce
  exact nativeQuantumSourceLaw_rejects_one
    (hforce 1 (namedPremises_all_couplings 1))

theorem nativeQuantumSourceLaw_unique
    (S₁ S₂ : ℝ)
    (h₁ : NativeQuantumSourceLaw S₁)
    (h₂ : NativeQuantumSourceLaw S₂) :
    S₁ = S₂ := by
  rw [(nativeQuantumSourceLaw_iff_inv S₁).mp h₁,
      (nativeQuantumSourceLaw_iff_inv S₂).mp h₂]

What this page does not claim

The one-act dual lock is not derived from the named premises alone. The theorem does not establish that the one-act dual is the only possible source law. The physical bridge from recognition events to actual particles is not claimed to be complete.

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