Foundation Unified Forcing Chain Canonical Seed Recognition Work Model Of Suppor

The support-event model

A support event is the primitive unit of recognition in this framework: a discrete record of which atoms are present in a single act of recognition. The declaration canonical_seed_recognition_work_model_of_support_events fixes the canonical model for how work is counted on such an event. It defines the cost of recognizing a support event as the cardinality of its support, that is, the number of atoms it contains. This is a definitional choice, a model, not a derived result.

What the framework proves is that this model is forced. The theorem supportEvent_support_cardinality_cost_unique states that any cost function on support events that satisfies the SupportCardinalityCost condition must equal the canonical support cost. In plain terms: if you require that the cost of recognizing an event is the size of its support, then there is exactly one way to assign that cost. The theorem is proved in the machine-checked library of formal theorems, and it is a genuine theorem, not a postulate.

The model sits inside a larger chain of forced results. The same library proves that any work composition operation satisfying the WorkExtensiveScaleComposition condition is unique, and that the seed size law holds: the levels of a seed-closed multilevel composition at the canonical post index equal the sum of the levels at indices zero and one. These results are part of the unified forcing chain that derives the golden ratio, the eight-tick cycle, and three spatial dimensions from the cost foundation.

What the declaration does not claim is that support events are the only way to model recognition, or that the cardinality cost is the only cost function that could be defined. It claims only that if you accept the SupportCardinalityCost condition, the cost is forced. The framework does not claim that support events exist in the physical world; it claims that if recognition is modeled this way, the mathematics is unique.

/-- Canonical recognition-work cost on support events: finite support
    cardinality. -/
def supportCost : CostFromDistinction.CostFunction (SupportEvent Atom) where
  C := fun a => (a.support.card : ℝ)
  nonneg := by
    intro a
    exact_mod_cast Nat.zero_le a.support.card
  dichotomy := by
    intro a
    constructor
    · intro h
      have hnat : a.support.card = 0 := by exact_mod_cast h
      exact Finset.card_eq_zero.mp hnat
    · intro h
      rw [h]
      simp
  additivity := by
    intro a b hindep
    change ((a.support ∪ b.support).card : ℝ) =
      (a.support.card : ℝ) + (b.support.card : ℝ)
    have hcard := Finset.card_union_of_disjoint hindep
    exact_mod_cast hcard

/-- Any support-cardinality cost on `SupportEvent` agrees pointwise with the
    canonical `SupportEvent.supportCost`. -/
theorem supportEvent_support_cardinality_cost_unique
    (Atom : Type) [DecidableEq Atom]
    (κ : CostFromDistinction.CostFunction (SupportEvent Atom))
    (hκ :
      SupportCardinalityCost
        (SupportEvent Atom) Atom κ SupportEvent.supportMap) :
    ∀ e : SupportEvent Atom, κ.C e = SupportEvent.supportCost.C e := by
  intro e
  rw [hκ.cost_eq_card e]
  rfl

/-- Work-extensive scale composition is unique as a binary operation. -/
theorem work_extensive_scale_composition_unique
    {op op' : ℝ → ℝ → ℝ}
    (h : WorkExtensiveScaleComposition op)
    (h' : WorkExtensiveScaleComposition op') :
    ∀ a b : ℝ, op a b = op' a b := by
  intro a b
  rw [h.work_extensive a b, h'.work_extensive a b]

/-- The seed-closed replacement has the seed size law by construction. -/
theorem seedClosedMultilevelComposition_seed_size_law
    (M : HierarchyForcing.NontrivialMultilevelComposition) :
    (seedClosedMultilevelComposition M).levels canonical_seed_post_index =
      (seedClosedMultilevelComposition M).levels 0 +
        (seedClosedMultilevelComposition M).levels 1 := by
  simp [seedClosedMultilevelComposition]

What this page does not claim

The declaration does not claim that support events are the only possible model of recognition. The declaration does not claim that the cardinality cost is the only definable cost function on support events. The declaration does not claim that support events exist as physical objects.

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