Foundation Pair Kernel Weyl Event Length Non Identifiability Same Present Weyl R

The scale wall

In the Recognition Science framework, a realized posting is a discrete record of a recognition event, carrying a clock center and a dimensionless localized radius. The declaration SamePresentWeylRecognitionData27 defines when two such records carry the same present data: they must share the same clock center and the same dimensionless radius. This is a definitional choice, a model of what counts as the information available at the present surface.

The framework's machine-checked library of formal theorems then proves a sharp negative result. Two records can share identical present data and still report different physical radii. The theorem presentWeylRecognitionData_does_not_select_dimensionedRadius27 shows that no amount of present data of this kind can select a unique physical length. The proof is constructive: for any carrier, there exists another carrier with the same present data but a different dimensioned radius. Positive rescaling of the physical event-length unit alone changes the reported radius while leaving the realized event, its center, and the dimensionless radius untouched.

This is a theorem no-go for the stated present-data interface, not a metatheoretic proof that no future Recognition construction can derive length. The surviving theory must add a scale-bearing physical carrier whose length response is part of the object from birth. The theorem names the exact uniqueness property that would be needed, PresentWeylRecognitionDataSelectsDimensionedRadius27, and proves it fails. The result is axiom-clean: no sorry, no new axiom, no empirical constant.

/-- Two positive length units remain compatible with exactly the same present
Weyl Recognition data and yield different physical radii. -/
theorem presentWeylRecognitionData_does_not_select_dimensionedRadius27
    {event : RealizedPostingEvent3 3}
    (carrier : RealizedPostingWeylLengthCarrier27 event) :
    ¬ PresentWeylRecognitionDataSelectsDimensionedRadius27
      carrier := by
  intro hselect
  have hsame :=
    scale_preserves_presentWeylRecognitionData27
      2 (by norm_num) carrier
  have heq := hselect
    (scaleRealizedPostingWeylLengthCarrier27
      2 (by norm_num) carrier) hsame
  rw [dimensionedWeylEventRadius_scale27] at heq
  have hradius_pos :
      0 < dimensionedWeylEventRadius27 carrier :=
    mul_pos carrier.eventLengthUnit_pos
      carrier.dimensionlessRadius_pos
  linarith

theorem scale_preserves_presentWeylRecognitionData27
    {event : RealizedPostingEvent3 3}
    (scale : ℝ)
    (hscale : 0 < scale)
    (carrier : RealizedPostingWeylLengthCarrier27 event) :
    SamePresentWeylRecognitionData27 carrier
      (scaleRealizedPostingWeylLengthCarrier27
        scale hscale carrier) := by
  exact ⟨rfl, rfl⟩

theorem dimensionedWeylEventRadius_scale27
    {event : RealizedPostingEvent3 3}
    (scale : ℝ)
    (hscale : 0 < scale)
    (carrier : RealizedPostingWeylLengthCarrier27 event) :
    dimensionedWeylEventRadius27
        (scaleRealizedPostingWeylLengthCarrier27
          scale hscale carrier) =
      scale * dimensionedWeylEventRadius27 carrier := by
  simp [dimensionedWeylEventRadius27,
    scaleRealizedPostingWeylLengthCarrier27]
  ring

/-- Two positive length units remain compatible with exactly the same present
Weyl Recognition data and yield different physical radii. -/
theorem presentWeylRecognitionData_does_not_select_dimensionedRadius27
    {event : RealizedPostingEvent3 3}
    (carrier : RealizedPostingWeylLengthCarrier27 event) :
    ¬ PresentWeylRecognitionDataSelectsDimensionedRadius27
      carrier := by
  intro hselect
  have hsame :=
    scale_preserves_presentWeylRecognitionData27
      2 (by norm_num) carrier
  have heq := hselect
    (scaleRealizedPostingWeylLengthCarrier27
      2 (by norm_num) carrier) hsame
  rw [dimensionedWeylEventRadius_scale27] at heq
  have hradius_pos :
      0 < dimensionedWeylEventRadius27 carrier :=
    mul_pos carrier.eventLengthUnit_pos
      carrier.dimensionlessRadius_pos
  linarith

What this page does not claim

This does not claim that no future Recognition construction can derive length. This does not claim that the dimensionless radius itself is unobservable. This does not claim that the clock center is not well-defined.

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