Foundation Pair Kernel Physical Source Law Identify Dual Eq Self Of One Act Phys

The one-act dual lock

The declaration identifyDual_eq_self_of_oneActPhysicalDual is a machine-checked theorem in the Recognition Science framework's library of formal theorems. It concerns a recognition event, a discrete record of an act of identification. The theorem states that for any one-act physical dual event, the dual that the event identifies is the event's own dual. In plainer terms: if a single act of recognition is set up so that the instrument's readout equals the curvature it measures, then the scale of that act is forced to be one, and the dual it picks out is itself, not something else.

The proof hinges on two steps. First, the framework proves that such an instrument must have a canonical unit, which forces the event's scale to be exactly one. Second, the identification function, when applied to scale one and any nonzero dual, returns that same dual. The theorem composes these two facts. The framework's library also proves a companion result: the same setup rejects scale two, so the one-act dual lock is not a choice between alternatives but a forced outcome of the curvature condition itself.

What the theorem does not claim is just as important. It does not claim that the one-act dual lock is the only possible source law. The framework's own documentation presents two candidate laws for absolute source scale. Candidate A is this one-act dual lock, which forces scale one. Candidate B is a different law, where the source magnitude equals the reciprocal of the native action quantum, which is the golden ratio raised to the fifth power. The library proves that these two candidates select distinct magnitudes, and that the named premises alone do not force either one. The theorem is a conditional statement: if a one-act physical dual event exists, then its scale is one and its dual is itself. It is not a proof that such an event must exist.

The framework's library also proves that the named premises, the basic assumptions of the framework, do not by themselves force the one-act dual lock. There is a residual gap: the attachment of the candidate predicate to the physical pair-kernel source object remains open. The reachability of a unique banked source magnitude is tagged as a hypothesis, not a theorem. This means the theorem is a precise but narrow result, a lock on a door that is not yet known to be the only door.

/-- Under Candidate A, dual identification collapses to the unscaled
coordinate. -/
theorem identifyDual_eq_self_of_oneActPhysicalDual
    (E : OneActDualEvent) (hE : IsOneActPhysicalDual E) :
    identifyDual E.scale E.dual = E.dual := by
  rw [oneActPhysicalDual_forces_scale_one E hE]
  simp [identifyDual]

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

theorem oneActPhysicalDual_rejects_two
    (E : OneActDualEvent) (hE : IsOneActPhysicalDual E) :
    E.scale ≠ 2 := by
  rw [oneActPhysicalDual_forces_scale_one E hE]
  norm_num

/-- 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

/-- 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

What this page does not claim

The theorem does not prove that a one-act physical dual event exists. The theorem does not derive the source magnitude from the named premises alone. The theorem does not identify which of the two candidate source laws is physically realized.

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: