Foundation Pair Kernel Gap2a Scale Breaking Phase Transaction Law Residual Scale

The scale-breaking residual

In the Recognition Science framework, physical structure is built from a discrete record of recognition events, called the ledger. The framework's machine-checked library of formal theorems has already attached a phase-bearing transaction to actual postings: eight theorem-backed Gray phases, one Tick per phase, exact closure after eight, and a linear aggregate for constant posting magnitude. The declaration scaleBreakingPhaseTransactionLaw_gap2a_residual is a theorem that sharpens the remaining obstruction to turning this into a physical law.

The theorem starts with two representatives of the same physical valuation. One has unit primitive-event action; the other has doubled action. Both carry identical Recognition-side data and fall into the same observable class. The theorem proves that for every one of the eight phases, the posting event action of the doubled representative is exactly twice that of the unit representative, and the two actions are never equal. This is the core fact: the same observable data admits two different action scales.

The declaration then proves a negative result about any proposed physical premise that could select between these two representatives. If a premise descends through the S20 observable quotient, meaning same Recognition data implies same premise verdict, and if it admits the unit representative, then no function of the observable class can recover all primitive phase actions under that premise. The same holds for a multiplicative action-dual source: no such descended premise can make it representative-independent. The library proves these impossibilities as theorems, not as conjectures.

The terminal theorem assembles these facts into a certificate. It states that the missing physical content is exactly a target-blind production premise that breaks, rather than descends through, the S20 positive action-scale torsor. In plain terms: any law strong enough to pick one action scale over the other must use physical information that the observable data does not contain. The declaration does not provide that premise; it names the precise gap and proves that the gap is real.

What this means for the framework is a sharpened research target. The eight-phase transaction is not yet a physical law because it cannot, by itself, choose a scale. The theorem converts a vague worry into a precise condition: the missing premise must break the S20 torsor. A reader can now see exactly what a successful law must add, and what any candidate that descends through S20 cannot achieve.

theorem phaseDoubledAction_phase_action_eq_two_mul
    (phase : Fin 8) :
    postingEventAction3 phaseDoubledActionValuation3.kinematics
        (phaseBearingPostingEvent3 phase).1 =
      2 *
        postingEventAction3 phaseUnitValuation3.kinematics
          (phaseBearingPostingEvent3 phase).1 := by
  unfold phaseDoubledActionValuation3
  simpa using
    (scalePhysicalValuation_eventAction
      2 1 (by norm_num) (by norm_num)
      phaseUnitValuation3
      (phaseBearingPostingEvent3 phase).1)

theorem phaseUnit_doubled_phase_action_ne
    (phase : Fin 8) :
    postingEventAction3 phaseUnitValuation3.kinematics
        (phaseBearingPostingEvent3 phase).1 ≠
      postingEventAction3 phaseDoubledActionValuation3.kinematics
        (phaseBearingPostingEvent3 phase).1 := by
  intro heq
  have hscaled :=
    phaseDoubledAction_phase_action_eq_two_mul phase
  rw [hscaled] at heq
  have hpos :
      0 <
        postingEventAction3 phaseUnitValuation3.kinematics
          (phaseBearingPostingEvent3 phase).1 :=
    mul_pos
      (phaseUnitValuation3.kinematics.energy_pos _)
      (phaseUnitValuation3.kinematics.duration_pos _)
  nlinarith

/-- If a phase-production premise still descends through S20 and admits the
already constructed unit representative, no observable-class action selector
can recover all primitive phase actions under that premise. -/
theorem no_S20_descended_phasePremise_recovers_absolutePhaseAction
    (premise : PhaseProductionPhysicalPremise3)
    (hdescends :
      PhaseProductionPremiseDescendsThroughS20 premise)
    (hunit : premise phaseUnitValuation3) :
    ¬ ∃ selector : PhasePremiseAbsoluteActionSelector3,
      SelectsPremisePhaseRepresentativeActions3
        premise selector := by
  rintro ⟨selector, hselector⟩
  have hdoubled : premise phaseDoubledActionValuation3 :=
    hdescends phaseUnitValuation3 phaseDoubledActionValuation3
      phaseUnit_doubled_sameRecognitionData hunit
  let phase : Fin 8 := 0
  have hleft :=
    hselector phaseUnitValuation3 hunit phase
  have hright :=
    hselector phaseDoubledActionValuation3 hdoubled phase
  rw [← phaseUnit_doubled_sameObservableClass] at hright
  have heq :
      postingEventAction3 phaseUnitValuation3.kinematics
          (phaseBearingPostingEvent3 phase).1 =
        postingEventAction3 phaseDoubledActionValuation3.kinematics
          (phaseBearingPostingEvent3 phase).1 :=
    hleft.symm.trans hright
  exact phaseUnit_doubled_phase_action_ne phase heq

/-- Terminal theorem for this pass: the missing physical content is exactly a
target-blind production premise that breaks, rather than descends through, the
S20 positive action-scale torsor. -/
theorem scaleBreakingPhaseTransactionLaw_gap2a_residual :
    Gap2aScaleBreakingPhaseTransactionLawResidualCert3 where
  actual_phase_transaction :=
    phaseBearingActualTransaction_cert
  same_observable_scaled_representative :=
    phaseUnit_doubled_sameObservableClass
  phase_action_changes_under_scaled_representative :=
    phaseUnit_doubled_phase_action_ne
  descended_premise_cannot_select_action :=
    no_S20_descended_phasePremise_recovers_absolutePhaseAction
  descended_premise_cannot_select_action_dual :=
    no_S20_descended_phasePremise_selects_actionDualSource

What this page does not claim

The declaration does not provide the missing physical premise that breaks the S20 torsor. The declaration does not prove that the eight-phase transaction is a complete physical law. The declaration does not claim that the S20 quotient is the only obstruction to a physical law.

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