Encyclopedia Foundation Foundation Pair Kernel Weyl Event Length Non Identifiability

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Weyl Event Length Non Identifiability

A machine-checked theorem shows that the present Recognition data cannot determine a physical length, forcing any future theory to carry scale from birth.

Verify this page

The scale wall

In physics, a length is a number with a unit attached: 1 meter, 3.2 light-years, 10^-35 planck lengths. The number alone means nothing without the unit, and the unit is a choice. Recognition Science, the framework that derives structure from a ledger of recognition events, ran into that choice as a wall. Its present data about an event, the clock center and a dimensionless radius, cannot by themselves pick out a physical length. The module that makes this precise is a theorem, machine-checked in the framework's library of formal theorems, with no unproved assumptions and no empirical constants.

The setup is plain. A length carrier holds two numbers: a dimensionless radius and a positive event-length unit. The physical radius is their product. The recognition data already present, the event's center and the dimensionless radius, are the same for two carriers that differ only in their unit. Rescale the unit by any positive factor, and the dimensionless radius stays fixed while the physical radius changes. The theorem proves that no such present data can select a unique physical radius: for any carrier, there exists another carrier with the same recognition data but a different physical radius. This is a constructive countermodel, not a gap in the proof.

The result is a no-go theorem for the stated interface, not a claim that length can never be derived. The framework's own documents say so explicitly. The surviving theory must add a scale-bearing physical carrier whose length response is part of the object from birth. The wall is exact, and the way through is specified: scale must enter as a primitive, not as a later addition.

THEOREM presentWeylRecognitionData_does_not_select_dimensionedRadius27 · presentWeylLengthScale_countermodel27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean
presentWeylRecognitionData_does_not_select_dimensionedRadius27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean:102 
/-- 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
presentWeylLengthScale_countermodel27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean:123 
/-- Constructive countermodel pair for external consumers. -/
theorem presentWeylLengthScale_countermodel27
    {event : RealizedPostingEvent3 3}
    (carrier : RealizedPostingWeylLengthCarrier27 event) :
    ∃ other : RealizedPostingWeylLengthCarrier27 event,
      SamePresentWeylRecognitionData27 carrier other ∧
        dimensionedWeylEventRadius27 carrier ≠
          dimensionedWeylEventRadius27 other := by
  refine
    ⟨scaleRealizedPostingWeylLengthCarrier27
        2 (by norm_num) carrier,
      scale_preserves_presentWeylRecognitionData27
        2 (by norm_num) carrier, ?_⟩
  intro heq
  rw [dimensionedWeylEventRadius_scale27] at heq
  have hradius_pos :
      0 < dimensionedWeylEventRadius27 carrier :=
    mul_pos carrier.eventLengthUnit_pos
      carrier.dimensionlessRadius_pos
  linarith
THEOREM dimensionedWeylEventRadius_scale27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean
dimensionedWeylEventRadius_scale27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean:79 
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
THEOREM presentWeylRecognitionData_does_not_select_dimensionedRadius27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean
presentWeylRecognitionData_does_not_select_dimensionedRadius27 · IndisputableMonolith/Foundation/PairKernelWeylEventLengthNonIdentifiability.lean:102 
/-- 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 length is fundamentally unknowable in Recognition Science. This does not claim that the theorem applies to any future Recognition construction that adds a scale-bearing carrier.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND