Foundation Pair Kernel Constructed Covector Event Occurrence Join Constructed Ev

The scale of a constructed source

The declaration constructedEventSourceCovector_scale_eq_constructedSourceScale is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that a particular mathematical object, called a constructed event source covector, acts on any test vector by multiplying the difference between the vector's values at two specific poles by a single number, the constructed source scale. In plainer terms, it proves that the source's response is completely characterized by one number, its scale, and that this number does not depend on which of the two possible ledger witnesses is used to define the source. The theorem is a formal proof that this scale is a property of the source itself, not of the observer's choice of representation.

This result is a step in a larger campaign to derive the Planck law from the framework's foundational principles. The theorem is a formal consequence of the definitions and prior theorems in the framework, and it is proved without any unproven assumptions. The proof is a simple equality, showing that the constructed object reduces to the product of the scale and a difference of the test vector's values at the source and sink poles. This is a structural result about the framework's constructions, not a claim about the physical world. It does not assert that the scale has any particular numerical value, nor that it corresponds to any measured physical quantity.

In Recognition Science, the framework models physical reality as a ledger, a discrete record of events. The theorem is part of a chain of reasoning that aims to show how the framework's abstract structures can give rise to familiar physical laws. The theorem is a formal statement about the framework's own definitions, and its significance is that it establishes a clean, observer-independent property of a constructed object. It is a piece of the framework's internal consistency, not a prediction that can be tested against experiment. The theorem's role is to ensure that the framework's constructions are well-behaved and that its derived quantities are well-defined.

The theorem does not claim that the framework has successfully derived the Planck law or any other physical law. That larger goal remains open. The theorem is a technical lemma, a step along the way, and its proof is a matter of formal logic, not empirical measurement. The framework's library is a collection of formal theorems, and this particular theorem is a contribution to that collection. It is a statement about the framework's own structures, and its value lies in the precision and rigor of its proof, not in any direct connection to the physical world.

/-- The instrument scale used by the event covector is the stage-1 constructed
scale.  It does not mention the witness. -/
theorem constructedEventSourceCovector_scale_eq_constructedSourceScale
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (event : RealizedPostingEvent3 N) (n : ℕ)
    (w : CommittedEventWitness event) (v : Fin (2 * 3) → ℝ) :
    constructedEventSourceCovector readout event n w v =
      constructedSourceScale readout event n *
        (v (polesOfCommittedWitness w).source -
          v (polesOfCommittedWitness w).sink) := by
  rfl

/-- Any two committed witnesses of the same event share the same instrument
scale factor (stage-1 scale).  Poles may differ. -/
theorem constructedEventSource_scale_witness_independent
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (event : RealizedPostingEvent3 N) (n : ℕ)
    (_w₁ _w₂ : CommittedEventWitness event) :
    constructedSourceScale readout event n =
      constructedSourceScale readout event n :=
  rfl

What this page does not claim

The theorem does not claim that the constructed source scale has any specific numerical value. The theorem does not claim that the framework has derived the Planck law or any other physical law. The theorem does not claim that the constructed source corresponds to any physical object.

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