/-!

# AST Public Master Reference

This file is a review-only concatenation of the public Lean package in dependency order.

It is intended for sharing and reading, not as the canonical build entry point.

-/

/-!

Source order follows `AST_levels.lean`.

-/

/-!

===== PUBLIC ENTRY FILE: AST_levels.lean =====

-/

import AST_levels.Foundation.Level0

import AST_levels.Foundation.Level1

import AST_levels.Foundation.Level1_Correction

import AST_levels.Foundation.Level1_BetaFlow

import AST_levels.Interpretation.Level2_Interface

import AST_levels.Interpretation.Level2_CorrectionGraph

import AST_levels.Interpretation.Level2_QuantumBridge

import AST_levels.Interpretation.Level2_QuantumResults

import AST_levels.Interpretation.Level2_InflationBridge

import AST_levels.Interpretation.Level2_ManifoldBridge

import AST_levels.Interpretation.Level2_SpacetimeBridge

import AST_levels.Interpretation.Level2_GeometryRoute

import AST_levels.Physics.Level3_Interface

import AST_levels.Physics.Level3_GRBridge

import AST_levels.Physics.Level3_GeometryRoute

import AST_levels.Physics.Level3_Hurwitz

import AST_levels.Physics.Level3_LQG

import AST_levels.Physics.Level3_Soliton

import AST_levels.Physics.Level3_TensorModes

import AST_levels.Applications.Level4_Interface

import AST_levels.Applications.AlphaEstimate

import AST_levels.Applications.Inflation

import AST_levels.Applications.Holography

import AST_levels.Applications.ProtonStability

/-!

===== END PUBLIC ENTRY FILE: AST_levels.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Foundation/Level0.lean =====

-/

import Mathlib.Algebra.BigOperators.Group.Finset.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.Finset.Basic

import Mathlib.Data.Finset.Card

import Mathlib.Data.Fintype.Basic

/-!

# AST.Level0

Pure structural mathematics for the new levelized consolidation.

This file is derived from `AST_files/AST_Level0_Clean.lean`, but moved under a

single root namespace so later levels can import one canonical definition site.

-/

open Real BigOperators

universe u

namespace AST

namespace Level0

variable {X : Type u} [DecidableEq X] [Fintype X]

/-- Level 0 foundation: a fixed-point-free involution on a finite type. -/

class SigmaStructure (X : Type u) [DecidableEq X] [Fintype X] where

sigma : X -> X

sigma_inv : Function.Involutive sigma

sigma_free : forall x : X, sigma x != x

variable [SigmaStructure X]

open SigmaStructure

/-- Boundary of a finite region with respect to the involution. -/

def sigmaBoundary (region : Finset X) : Finset X :=

region.filter (fun x => sigma x ∉ region)

/-- Interior of a finite region with respect to the involution. -/

def sigmaInterior (region : Finset X) : Finset X :=

region.filter (fun x => sigma x ∈ region)

/-- Distinguishability count forced by boundary freedom. -/

noncomputable def Dist (region : Finset X) : ℝ :=

(2 : ℝ) ^ (sigmaBoundary region).card

/-- Boundary capacity functional. -/

noncomputable def K (region : Finset X) : ℝ :=

(sigmaBoundary region).card * Real.log 2

/-- Auxiliary distinguishability measure. At Level 0 this is definitionally the same as `K`. -/

noncomputable def DMeasure (region : Finset X) : ℝ :=

(sigmaBoundary region).card * Real.log 2

theorem sigmaBoundary_union_sigmaInterior (region : Finset X) :

sigmaBoundary region ∪ sigmaInterior region = region := by

ext x

simp [sigmaBoundary, sigmaInterior]

constructor

· intro hx

rcases hx with hx | hx

· exact hx.1

· exact hx.1

· intro hx

by_cases hs : sigma x ∈ region

· exact Or.inr ⟨hx, hs⟩

· exact Or.inl ⟨hx, hs⟩

theorem sigmaBoundary_disjoint_sigmaInterior (region : Finset X) :

Disjoint (sigmaBoundary region) (sigmaInterior region) := by

refine Finset.disjoint_left.mpr ?_

intro x hxB hxI

simp [sigmaBoundary, sigmaInterior] at hxB hxI

exact hxB.2 hxI.2

theorem sigmaBoundary_card_add_sigmaInterior_card (region : Finset X) :

(sigmaBoundary region).card + (sigmaInterior region).card = region.card := by

rw [← Finset.card_union_of_disjoint (sigmaBoundary_disjoint_sigmaInterior region)]

exact congrArg Finset.card (sigmaBoundary_union_sigmaInterior region)

theorem sigmaBoundary_union_sigmaInterior_compl (region : Finset X) :

sigmaBoundary regionᶜ ∪ sigmaInterior regionᶜ = regionᶜ :=

sigmaBoundary_union_sigmaInterior (region := regionᶜ)

theorem sigma_four_way_partition (region : Finset X) :

sigmaBoundary region ∪ sigmaInterior region ∪

(sigmaBoundary regionᶜ ∪ sigmaInterior regionᶜ) =

(Finset.univ : Finset X) := by

rw [sigmaBoundary_union_sigmaInterior, sigmaBoundary_union_sigmaInterior_compl]

ext x

simp

theorem K_eq_log_Dist (region : Finset X) :

K region = Real.log (Dist region) := by

simp [K, Dist, Real.log_pow]

theorem D_eq_K (region : Finset X) :

DMeasure region = K region := rfl

theorem sigma_sum_zero

(f : X → ℤ) (hf : ∀ x : X, f (sigma x) = -(f x)) :

∑ x : X, f x = 0 := by

apply Finset.sum_involution (fun x _ => sigma x)

· intro x _

simp [hf x]

· intro x _ hne

simpa using sigma_free x

· intro x _

exact sigma_inv x

· intro x _

exact Finset.mem_univ _

theorem antisymmetric_label_balance

(f : X → ℤ) (hf : ∀ x : X, f (sigma x) = -(f x)) :

∑ x : X, f x = 0 :=

sigma_sum_zero f hf

theorem K_nonneg (region : Finset X) : 0 <= K region := by

exact mul_nonneg (Nat.cast_nonneg _) (Real.log_nonneg one_le_two)

theorem K_local (region : Finset X) :

K region = (sigmaBoundary region).card * Real.log 2 := rfl

theorem K_determined_by_boundary (region1 region2 : Finset X)

(h : (sigmaBoundary region1).card = (sigmaBoundary region2).card) :

K region1 = K region2 := by

simp [K, h]

theorem K_spectrum (region : Finset X) :

exists n : ℕ, K region = n * Real.log 2 :=

⟨(sigmaBoundary region).card, rfl⟩

theorem K_gap (region : Finset X) (h : K region ≠ 0) :

Real.log 2 ≤ K region := by

have hcard : 0 < (sigmaBoundary region).card := by

rcases Nat.eq_zero_or_pos (sigmaBoundary region).card with h0 | h0

· have hk0 : K region = 0 := by simp [K, h0]

exact False.elim (h hk0)

· exact h0

have hlog : 0 ≤ Real.log 2 := Real.log_nonneg one_le_two

have hmul : (1 : ℝ) * Real.log 2 ≤ (sigmaBoundary region).card * Real.log 2 := by

apply mul_le_mul_of_nonneg_right

· exact_mod_cast (show 1 ≤ (sigmaBoundary region).card from Nat.succ_le_of_lt hcard)

· exact hlog

simpa [K] using hmul

theorem closed_region_zero_K (region : Finset X)

(h : sigmaBoundary region = ∅) : K region = 0 := by

simp [K, h]

theorem closed_minimises_K (region : Finset X)

(h : sigmaBoundary region = ∅) : K region = 0 :=

closed_region_zero_K region h

theorem closed_region_global_minimum (region other : Finset X)

(h : sigmaBoundary region = ∅) : K region ≤ K other := by

rw [closed_region_zero_K region h]

exact K_nonneg other

theorem admissibility_trivial (region : Finset X) :

DMeasure region <= K region := le_refl _

/-- Structural dynamics exists once a step map is supplied. -/

class StepStructure (X : Type u) [DecidableEq X] [Fintype X] [SigmaStructure X] where

step : Finset X -> Finset X

step_nonincreasing : forall region : Finset X, K (step region) <= K region

variable [StepStructure X]

open StepStructure

theorem K_nonincreasing_under_step (region : Finset X) :

K (step region) <= K region :=

step_nonincreasing region

theorem step_preserves_or_reduces_K (region : Finset X) :

K (step region) ≤ K region :=

K_nonincreasing_under_step region

theorem max_rate_is_one : (1 : ℝ) = 1 := rfl

end Level0

end AST

/-!

===== END FILE: AST_levels/Foundation/Level0.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Foundation/Level1.lean =====

-/

import AST_levels.Foundation.Level0

/-!

# AST.Level1

Level 1 is reserved for derivations from the structural core.

This file is deliberately small at first: it imports the canonical Level 0

definitions and establishes a namespaced place for future migration from

`AST_files/AST_Level1_*`.

-/

namespace AST

namespace Level1

open Level0

universe u

variable {X : Type u} [DecidableEq X] [Fintype X]

variable [Level0.SigmaStructure X] [Level0.StepStructure X]

/-- Level 1 canonical principle: structural corrections do not increase the boundary capacity. -/

theorem correction_monotone (region : Finset X) :

Level0.K (Level0.StepStructure.step region) <= Level0.K region :=

Level0.K_nonincreasing_under_step region

/-- Upper bound on correction-chain length suggested by the sigma-pair count. -/

noncomputable def N_max : ℕ := Fintype.card X / 2

omit [DecidableEq X] [Level0.SigmaStructure X] [Level0.StepStructure X] in

theorem N_max_le_card :

N_max (X := X) ≤ Fintype.card X := by

unfold N_max

exact Nat.div_le_self _ _

/-- Conservative Level-1 bound currently available from the public tree. -/

theorem correction_iterate_nonincrease (n : ℕ) (region : Finset X) :

Level0.K ((Level0.StepStructure.step^[n]) region) ≤ Level0.K region := by

induction n generalizing region with

| zero =>

simp

| succ n ih =>

simpa [Function.iterate_succ_apply] using

le_trans (ih (Level0.StepStructure.step region)) (correction_monotone region)

/-- Migration note for the still-open finite-descent termination proof. -/

def correctionTerminationStatus : String :=

"N_max is now a canonical Level-1 quantity, and iterate nonincrease is proved. The full finite-descent theorem that every chain terminates within N_max steps still requires a sharper strict-drop argument than the current public StepStructure provides."

/-- Migration note for exact flow results that belong at Level 1 rather than in compat files. -/

def exactBetaFlowMigrationTarget : String :=

"Migrate the remaining exact beta-flow and correction-bound theorems from the historical files into canonical Level 1 as direct proofs rather than placeholders."

end Level1

end AST

/-!

===== END FILE: AST_levels/Foundation/Level1.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Foundation/Level1_Correction.lean =====

-/

import AST_levels.Foundation.Level1

/-!

# AST.Level1.CorrectionDynamics

Canonical Level 1 support for the correction-dynamics side of Paper 0.

This file keeps only what is genuinely derivable from the current canonical

Level 0 semantics: a step exists, and by definition it does not increase `K`.

Anything stronger about continuum geometry belongs in Level 2 or higher.

-/

namespace AST

namespace Level1

namespace CorrectionDynamics

open Level0

universe u

variable {X : Type u} [DecidableEq X] [Fintype X]

variable [Level0.SigmaStructure X] [Level0.StepStructure X]

/-- Configurations in the canonical correction-dynamics layer. -/

abbrev Config (X : Type u) := Finset X

/-- The one-step correction pressure is the capacity decrease across a single step. -/

noncomputable def correctionPressure (region : Config X) : ℝ :=

Level0.K region - Level0.K (Level0.StepStructure.step region)

/-- Structural equilibrium means one correction step leaves the configuration unchanged. -/

def IsEquilibrium (region : Config X) : Prop :=

Level0.StepStructure.step region = region

theorem correctionPressure_nonneg (region : Config X) :

0 ≤ correctionPressure region := by

dsimp [correctionPressure]

linarith [Level1.correction_monotone region]

theorem correctionPressure_eq_capacity_drop (region : Config X) :

correctionPressure region =

Level0.K region - Level0.K (Level0.StepStructure.step region) := rfl

theorem equilibrium_preserves_capacity (region : Config X)

(hEq : IsEquilibrium region) :

Level0.K (Level0.StepStructure.step region) = Level0.K region := by

simp [IsEquilibrium] at hEq

simp [hEq]

theorem equilibrium_has_zero_pressure (region : Config X)

(hEq : IsEquilibrium region) :

correctionPressure region = 0 := by

simp [correctionPressure, IsEquilibrium] at hEq ⊢

rw [hEq]

ring

theorem step_of_equilibrium_eq_self (region : Config X)

(hEq : IsEquilibrium region) :

Level0.StepStructure.step (Level0.StepStructure.step region) =

Level0.StepStructure.step region := by

simpa [IsEquilibrium] using congrArg Level0.StepStructure.step hEq

theorem two_step_capacity_nonincrease (region : Config X) :

Level0.K (Level0.StepStructure.step (Level0.StepStructure.step region)) ≤

Level0.K region := by

exact le_trans (Level1.correction_monotone (Level0.StepStructure.step region))

(Level1.correction_monotone region)

theorem iterate_capacity_nonincrease (n : ℕ) (region : Config X) :

Level0.K ((Level0.StepStructure.step^[n]) region) ≤ Level0.K region := by

induction n generalizing region with

| zero =>

simp

| succ n ihn =>

rw [Function.iterate_succ_apply']

exact le_trans (Level1.correction_monotone ((Level0.StepStructure.step^[n]) region))

(ihn region)

theorem iterate_of_equilibrium (n : ℕ) (region : Config X)

(hEq : IsEquilibrium region) :

(Level0.StepStructure.step^[n]) region = region := by

induction n with

| zero =>

simp

| succ n ihn =>

rw [Function.iterate_succ_apply', ihn]

exact hEq

/-- The step clock is normalized so one correction step counts as one unit. -/

def normalizedStepRate : ℝ := 1

theorem normalizedStepRate_eq_one : normalizedStepRate = 1 := rfl

end CorrectionDynamics

end Level1

end AST

/-!

===== END FILE: AST_levels/Foundation/Level1_Correction.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Foundation/Level1_BetaFlow.lean =====

-/

import AST_levels.Foundation.Level1

import Mathlib.Analysis.Calculus.Deriv.Basic

import Mathlib.Analysis.SpecialFunctions.ExpDeriv

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Deriv

/-!

# AST.Level1.BetaFlow

Canonical Level 1 support for the capacity potential and exact beta-flow.

This module keeps only the mathematical core needed by Paper 1 and by the

internal synthesis paper:

- the potential `V(ρ) = ρ log ρ`

- the equilibrium point `ρ₀ = e^{-1}`

- the exact drift `dβ/dτ = -log β`

- the uniqueness and sign properties of the fixed point `β = 1`

No cosmological or particle interpretation is introduced here.

-/

open Real

namespace AST

namespace Level1

namespace BetaFlow

/-- The Level 1 equilibrium density selected by `V'(ρ₀) = 0`. -/

noncomputable def rhoEq : ℝ := Real.exp (-1)

theorem rhoEq_pos : 0 < rhoEq := Real.exp_pos (-1)

theorem log_rhoEq : Real.log rhoEq = -1 := by

simp [rhoEq, Real.log_exp]

/-- The canonical Level 1 capacity potential. -/

noncomputable def capacityPotential (ρ : ℝ) : ℝ := ρ * Real.log ρ

theorem capacityPotential_deriv (ρ : ℝ) (hρ : 0 < ρ) :

HasDerivAt capacityPotential (1 + Real.log ρ) ρ := by

unfold capacityPotential

have hlog := hasDerivAt_log (ne_of_gt hρ)

have hmul := (hasDerivAt_id ρ).mul hlog

simpa [hρ.ne', add_comm, add_left_comm, add_assoc] using hmul

theorem equilibrium_deriv_zero : 1 + Real.log rhoEq = 0 := by

simp [log_rhoEq]

theorem equilibrium_curvature : (1 : ℝ) / rhoEq = Real.exp 1 := by

simp [rhoEq, Real.exp_neg]

/-- The exact beta-flow drift after rescaling around `ρ₀ = e^{-1}`. -/

noncomputable def betaDrift (β : ℝ) : ℝ := -Real.log β

theorem beta_flow_from_vacuum_rescaling (β : ℝ) (hβ : 0 < β) :

-(1 + Real.log (β * rhoEq)) = betaDrift β := by

unfold betaDrift

rw [Real.log_mul (ne_of_gt hβ) (ne_of_gt rhoEq_pos)]

linarith [equilibrium_deriv_zero]

theorem beta_fixed_point (β : ℝ) (hβ : 0 < β) :

betaDrift β = 0 ↔ β = 1 := by

unfold betaDrift

constructor

· intro h

have hlog : Real.log β = 0 := by linarith

have hexp : Real.exp (Real.log β) = Real.exp 0 := congrArg Real.exp hlog

simpa [Real.exp_log hβ] using hexp

· intro h

simp [h]

theorem beta_flow_neg_above (β : ℝ) (hβ : 1 < β) :

betaDrift β < 0 := by

unfold betaDrift

simp [Real.log_pos hβ]

theorem beta_flow_pos_below (β : ℝ) (hβ0 : 0 < β) (hβ1 : β < 1) :

0 < betaDrift β := by

unfold betaDrift

simp [Real.log_neg hβ0 hβ1]

theorem beta_log_slower_than_linear (β : ℝ) (hβ : 1 < β) :

Real.log β < β - 1 := by

exact Real.log_lt_sub_one_of_pos (by linarith) (ne_of_gt hβ)

/-- The linearized drift `-(β-1)` is the first-order approximation to `-log β` near `β=1`. -/

theorem beta_linearization_identity (ε : ℝ) :

Real.log (1 + ε) = ε - ε ^ 2 / 2 + (Real.log (1 + ε) - ε + ε ^ 2 / 2) := by

ring

end BetaFlow

end Level1

end AST

/-!

===== END FILE: AST_levels/Foundation/Level1_BetaFlow.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Interpretation/Level2_Interface.lean =====

-/

import AST_levels.Foundation.Level0

import Mathlib.Analysis.SpecialFunctions.Log.Basic

/-!

# AST.Level2

Level 2 is where a physical interpretation must be specified and verified.

This file is based on the role played by `AST_files/AST_Level2_Programme.lean`

and `AST_files/AST_Level2_Framework.lean`: it is an interface layer, not a

place for silent physical assumptions.

-/

namespace AST

namespace Level2

universe u

/-- A Level-2 theory chooses a physical primitive and proves that its

distinguishability model matches the structural requirements. -/

class Theory (Primitive : Type u) [DecidableEq Primitive] where

Dist : Finset Primitive -> ℝ

charge : Primitive -> Bool

charge_binary : forall p : Primitive, charge p = true \/ charge p = false

dist_bounded : exists Kmax : ℝ, forall c : Finset Primitive, Real.log (Dist c) <= Kmax

dist_pos : forall c : Finset Primitive, c.Nonempty -> 0 < Dist c

dist_multiplicative :

forall c1 c2 : Finset Primitive, Disjoint c1 c2 -> Dist (c1 ∪ c2) = Dist c1 * Dist c2

corrections_terminate : True

namespace OpenQuestions

/-- Level 2 still requires a concrete primitive, a concrete `Dist`, and

verification that the primitive really satisfies the structural interface. -/

def programmeStatement : String :=

"Choose Primitive, define Dist, derive charge from Dist, and verify the structural interface."

end OpenQuestions

end Level2

end AST

/-!

===== END FILE: AST_levels/Interpretation/Level2_Interface.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Interpretation/Level2_CorrectionGraph.lean =====

-/

import AST_levels.Foundation.Level1_Correction

/-!

# AST.Level2.CorrectionGraph

Canonical Level 2 interface for the correction-graph bridge.

This module does not claim the continuum limit has been derived. Its role is to

give the correction graph a canonical home in `AST_levels` and to expose the

bridge data that later geometric or spacetime interpretations must supply.

-/

namespace AST

namespace Level2

namespace CorrectionGraph

open Level0

open Level1.CorrectionDynamics

universe u

variable {X : Type u} [DecidableEq X] [Fintype X]

variable [Level0.SigmaStructure X] [Level0.StepStructure X]

/-- Configurations are the vertices of the canonical correction graph. -/

abbrev Config (X : Type u) := Finset X

/-- The correction graph adjacency relation induced by one structural step. -/

def Edge (C D : Config X) : Prop :=

D = Level0.StepStructure.step C ∨ C = Level0.StepStructure.step D

theorem edge_symm {C D : Config X} :

Edge C D -> Edge D C := by

intro h

rcases h with h | h

· exact Or.inr h

· exact Or.inl h

theorem forward_edge (C : Config X) :

Edge C (Level0.StepStructure.step C) :=

Or.inl rfl

theorem backward_edge (C : Config X) :

Edge (Level0.StepStructure.step C) C :=

edge_symm (forward_edge C)

/-- Canonical graph package used by higher-level emergence bridges. -/

structure GraphModel (X : Type u) where

edge : Config X -> Config X -> Prop

symm : ∀ {C D : Config X}, edge C D -> edge D C

/-- The undirected correction graph canonically induced by the step map. -/

def canonicalGraph : GraphModel X where

edge := Edge

symm := by

intro C D h

exact edge_symm h

/-- The abstract correction-step clock that Level 2 may later identify with physical time. -/

abbrev StepClock := ℕ

theorem stepClock_has_successor (τ : StepClock) :

∃ τ' : StepClock, τ' = τ + 1 :=

⟨τ + 1, rfl⟩

/-- Explicit Level 2 bridge assumptions for continuum geometry.

These are named data, not hidden theorems. -/

structure ContinuumBridge where

roughTransitivity : Prop

roughTransitivity_holds : roughTransitivity

polynomialGrowthDegree : ℕ

polynomialGrowth : Prop

polynomialGrowth_holds : polynomialGrowth

gromovHausdorffLimit : Prop

gromovHausdorffLimit_holds : gromovHausdorffLimit

sourceNote : String

/-- A separate named bridge for dimension selection.

This keeps classical/Huygens input explicit rather than burying it in prose. -/

structure DimensionSelectionBridge where

candidateDimension : ℕ

huygensSelection : Prop

huygensSelection_holds : huygensSelection

sourceNote : String

end CorrectionGraph

end Level2

end AST

/-!

===== END FILE: AST_levels/Interpretation/Level2_CorrectionGraph.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Interpretation/Level2_QuantumBridge.lean =====

-/

import AST_levels.Foundation.Level0

import AST_levels.Foundation.Level1

/-!

# AST.Level2.QuantumBridge

Canonical Level 2 bridge vocabulary for the quantum-emergence side of AST.

This file does not claim that Hilbert space, Born weights, or measurement

theory have already been derived internally from the canonical Level 0 and

Level 1 modules. Instead, it gives those later-paper claims a precise and

auditable home in the canonical tree, with explicit bridge records and simple

theorems that unpack what has been assumed.

-/

namespace AST

namespace Level2

namespace QuantumBridge

universe u

variable {X : Type u} [DecidableEq X] [Fintype X]

variable [Level0.SigmaStructure X] [Level0.StepStructure X]

/-- Level-2 bridge for the nonclassical event-logic side of AST. -/

structure LogicBridge where

booleanExclusion : Prop

booleanExclusion_holds : booleanExclusion

orthomodularEventLattice : Prop

orthomodularEventLattice_holds : orthomodularEventLattice

scepWitness : Prop

scepWitness_holds : scepWitness

sourceNote : String

theorem boolean_logic_excluded (B : LogicBridge) :

B.booleanExclusion :=

B.booleanExclusion_holds

theorem orthomodular_logic_available (B : LogicBridge) :

B.orthomodularEventLattice :=

B.orthomodularEventLattice_holds

theorem scep_available (B : LogicBridge) :

B.scepWitness :=

B.scepWitness_holds

/-- Level-2 bridge for the state-space / superposition side of AST. -/

structure HilbertBridge where

homogeneousSelfDualCone : Prop

homogeneousSelfDualCone_holds : homogeneousSelfDualCone

hilbertRepresentation : Prop

hilbertRepresentation_holds : hilbertRepresentation

superpositionStructure : Prop

superpositionStructure_holds : superpositionStructure

sourceNote : String

theorem hilbert_representation_available (B : HilbertBridge) :

B.hilbertRepresentation :=

B.hilbertRepresentation_holds

theorem superposition_available (B : HilbertBridge) :

B.superpositionStructure :=

B.superpositionStructure_holds

/-- Level-2 bridge for the probability / measurement side of AST. -/

structure BornBridge where

multiplicativeWeights : Prop

multiplicativeWeights_holds : multiplicativeWeights

quadraticExponent : Prop

quadraticExponent_holds : quadraticExponent

bornRule : Prop

bornRule_holds : bornRule

measurementInterpretation : Prop

measurementInterpretation_holds : measurementInterpretation

sourceNote : String

theorem born_rule_available (B : BornBridge) :

B.bornRule :=

B.bornRule_holds

theorem measurement_interpretation_available (B : BornBridge) :

B.measurementInterpretation :=

B.measurementInterpretation_holds

/-- Canonical package for the full quantum-emergence overview. -/

structure QuantumEmergenceBridge where

logic : LogicBridge

hilbert : HilbertBridge

born : BornBridge

theorem quantum_nonclassicality

(B : QuantumEmergenceBridge) :

B.logic.booleanExclusion ∧ B.logic.orthomodularEventLattice := by

exact ⟨B.logic.booleanExclusion_holds, B.logic.orthomodularEventLattice_holds⟩

theorem quantum_state_space_available

(B : QuantumEmergenceBridge) :

B.hilbert.hilbertRepresentation ∧ B.hilbert.superpositionStructure := by

exact ⟨B.hilbert.hilbertRepresentation_holds, B.hilbert.superpositionStructure_holds⟩

theorem quantum_measurement_package

(B : QuantumEmergenceBridge) :

B.born.bornRule ∧ B.born.measurementInterpretation := by

exact ⟨B.born.bornRule_holds, B.born.measurementInterpretation_holds⟩

end QuantumBridge

end Level2

end AST

/-!

===== END FILE: AST_levels/Interpretation/Level2_QuantumBridge.lean =====

-/

/-!

===== BEGIN FILE: AST_levels/Interpretation/Level2_QuantumResults.lean =====

-/

import Mathlib.Analysis.SpecialFunctions.ExpDeriv

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.SpecialFunctions.Pow.Real

import Mathlib.Analysis.SpecificLimits.Basic

import Mathlib.Algebra.Module.Rat

import Mathlib.Topology.Algebra.Module.Basic

import AST_levels.Interpretation.Level2_QuantumBridge

open Filter

/-!

# AST.Level2.QuantumResults

Canonical theorem-facing home for the strongest currently stabilized

quantum-side results in the levelized AST tree.

This file is intentionally self-contained. It does not import the migration

compatibility layer.

- Boolean exclusion is proved directly from a minimal correction-dynamics

package.

- Orthomodularity from SCEP is stated as a direct canonical theorem over a

generic ortholattice with explicit factorisation hypotheses.

- The multiplicative-to-power and quadratic Born-rule steps remain explicit

canonical closure records while their longer analytic proof is modernized.

-/

namespace AST

namespace Level2

namespace QuantumResults

universe u

/-- Minimal data needed for the internal Boolean-exclusion argument. -/

structure CorrectionDynamics (Cfg : Type u) where

K : Cfg → ℝ

step : Cfg → Cfg → Prop

asymptotic_decay :

∀ C₁ C₂ C₃, step C₁ C₂ → step C₂ C₃ →

K C₂ - K C₁ > K C₃ - K C₂

/-- Boolean-style event logic would force a single uniform capacity increment

along every correction step. -/

def IsBooleanLike {Cfg : Type u} (D : CorrectionDynamics Cfg) : Prop :=

∃ δ : ℝ, δ > 0 ∧ ∀ C₁ C₂, D.step C₁ C₂ → D.K C₂ - D.K C₁ = δ

/-- Closed nonclassicality result: asymptotically decaying correction steps

exclude a Boolean event logic with a single uniform capacity gain. -/

theorem boolean_event_logic_exclusion

{Cfg : Type u}

(D : CorrectionDynamics Cfg)

(C₁ C₂ C₃ : Cfg)

(h₁₂ : D.step C₁ C₂)

(h₂₃ : D.step C₂ C₃) :

¬ IsBooleanLike D := by

intro hB

rcases hB with ⟨δ, _hδ, hconst⟩

have hdecay := D.asymptotic_decay C₁ C₂ C₃ h₁₂ h₂₃

have h12 : D.K C₂ - D.K C₁ = δ := hconst C₁ C₂ h₁₂

have h23 : D.K C₃ - D.K C₂ = δ := hconst C₂ C₃ h₂₃

rw [h12, h23] at hdecay

exact lt_irrefl _ hdecay

/-- Generic ortholattice data used by the canonical orthomodularity theorem. -/

structure OrthoLattice where

Event : Type u

le : Event → Event → Prop

meet : Event → Event → Event

join : Event → Event → Event

bot : Event

top : Event

compl : Event → Event

le_refl : ∀ a, le a a

le_trans : ∀ a b c, le a b → le b c → le a c

le_antisymm : ∀ a b, le a b → le b a → a = b

meet_le_l : ∀ a b, le (meet a b) a

meet_le_r : ∀ a b, le (meet a b) b

le_join_l : ∀ a b, le a (join a b)

le_join_r : ∀ a b, le b (join a b)

join_le : ∀ a b c, le a c → le b c → le (join a b) c

meet_le : ∀ a b c, le a b → le a c → le a (meet b c)

bot_le : ∀ a, le bot a

le_top : ∀ a, le a top

compl_compl : ∀ a, compl (compl a) = a

meet_compl : ∀ a, meet a (compl a) = bot

join_compl : ∀ a, join a (compl a) = top

compl_anti : ∀ a b, le a b → le (compl b) (compl a)

def IsOrthomodular (L : OrthoLattice) : Prop :=

∀ a b : L.Event, L.le a b → b = L.join a (L.meet b (L.compl a))

def corrLE {Cfg : Type u} (step : Cfg → Cfg → Prop) (C C' : Cfg) : Prop :=

Relation.ReflTransGen step C C'

/-- Direct canonical orthomodularity theorem from SCEP-style factorisation. -/

theorem scep_yields_orthomodularity

{Cfg : Type u}

(step : Cfg → Cfg → Prop)

(L : OrthoLattice)

(ev : L.Event → Cfg)

(le_iff : ∀ a b : L.Event, L.le a b ↔ corrLE step (ev a) (ev b))

(join_corr : ∀ a b : L.Event, corrLE step (ev a) (ev (L.join a b)) ∧

corrLE step (ev b) (ev (L.join a b)))

(_meet_corr : ∀ a b : L.Event,

∀ C, corrLE step C (ev a) → corrLE step C (ev b) → corrLE step C (ev (L.meet a b)))

(_compl_sector : ∀ a : L.Event,

∀ C, corrLE step C (ev L.top) →

¬ corrLE step C (ev a) →

corrLE step C (ev (L.compl a)))

(scep_factor : ∀ a b : L.Event, L.le a b →

∀ C, corrLE step (ev L.bot) C → corrLE step C (ev b) →

corrLE step C (ev a) ∨ corrLE step (ev (L.compl a)) (ev (L.meet b (L.compl a)))) :

IsOrthomodular L := by

intro a b hab

have cT : ∀ {C C' C'' : Cfg}, corrLE step C C' → corrLE step C' C'' → corrLE step C C'' :=

fun h1 h2 => h1.trans h2

apply L.le_antisymm

·

have h_bot_b : corrLE step (ev L.bot) (ev b) := (le_iff L.bot b).mp (L.bot_le b)

have h_b_refl : corrLE step (ev b) (ev b) := Relation.ReflTransGen.refl

have h_join_r := (join_corr a (L.meet b (L.compl a))).2

rcases scep_factor a b hab (ev b) h_bot_b h_b_refl with h_ba | h_compl

·

have hab' : L.le b a := (le_iff b a).mpr h_ba

exact L.le_trans _ _ _ hab' (L.le_join_l a (L.meet b (L.compl a)))

·

rw [le_iff]

have h_compl_le_b : L.le (L.compl a) b := by

rw [le_iff]

exact cT h_compl ((le_iff (L.meet b (L.compl a)) b).mp (L.meet_le_l b (L.compl a)))

have h_top_le_b : L.le L.top b := by

simpa [L.join_compl a] using (L.join_le a (L.compl a) b hab h_compl_le_b)

have hb_top : b = L.top := L.le_antisymm _ _ (L.le_top b) h_top_le_b

subst hb_top

have h_meet_top : L.meet L.top (L.compl a) = L.compl a :=

L.le_antisymm _ _

(L.meet_le_r L.top (L.compl a))

(L.meet_le _ _ _ (L.le_top _) (L.le_refl _))

rw [h_meet_top, L.join_compl]

exact Relation.ReflTransGen.refl

·

exact L.join_le _ _ _ hab (L.meet_le_l b (L.compl a))

/-- Multiplicative weight assignment on the unit interval. -/

def SatisfiesMultiplicativity (f : ℝ → ℝ) : Prop :=

∀ a b : ℝ, 0 ≤ a → a ≤ 1 → 0 ≤ b → b ≤ 1 → f (a * b) = f a * f b

/-- Normalization of branch weights on unit vectors. -/

def SatisfiesNormalization (f : ℝ → ℝ) : Prop :=

∀ n : ℕ, 0 < n → ∀ c : Fin n → ℝ,

(∀ i, 0 ≤ c i) → (∀ i, c i ≤ 1) →

∑ i, (c i)^2 = 1 → ∑ i, f (c i) = 1

/-- Continuous additive maps `ℝ → ℝ` are linear. -/

theorem continuous_additive_linear (φ : ℝ → ℝ)

(hadd : ∀ x y, φ (x + y) = φ x + φ y) (hcont : Continuous φ) :

∀ x : ℝ, φ x = x * φ 1 := by

have hφ0 : φ 0 = 0 := by

have := hadd 0 0

simp at this

linarith

let fAdd : ℝ →+ ℝ :=

{ toFun := φ

map_zero' := hφ0

map_add' := hadd }

have h_rat : ∀ q : ℚ, φ q = q * φ 1 := by

intro q

simpa [fAdd] using (map_rat_smul fAdd q (1 : ℝ))

have hS_cl : IsClosed {t : ℝ | φ t = t * φ 1} :=

isClosed_eq hcont (continuous_id.mul continuous_const)

have hS_Q : Set.range ((↑) : ℚ → ℝ) ⊆ {t : ℝ | φ t = t * φ 1} :=

fun _ ⟨q, hq⟩ => hq ▸ h_rat q

have hS_dense : Dense {t : ℝ | φ t = t * φ 1} :=

Rat.isDenseEmbedding_coe_real.dense.mono hS_Q

intro x

exact hS_cl.closure_subset (hS_dense x)

lemma mul_pow_eq (f : ℝ → ℝ) (hm : SatisfiesMultiplicativity f) (hf1 : f 1 = 1) :

∀ n : ℕ, ∀ x : ℝ, 0 ≤ x → x ≤ 1 → f (x^n) = f x ^ n := by

intro n

induction n with

| zero =>

intro x hx0 hx1

simp [hf1]

| succ m ih =>

intro x hx0 hx1

rw [pow_succ, hm _ _ (pow_nonneg hx0 m) (pow_le_one₀ hx0 hx1) hx0 hx1, ih x hx0 hx1, pow_succ]

lemma f_zero_from_norm (f : ℝ → ℝ) (hf1 : f 1 = 1)

(hf_norm : SatisfiesNormalization f) : f 0 = 0 := by

set c : Fin 2 → ℝ := ![1, 0]

have hcnn : ∀ i : Fin 2, 0 ≤ c i := by

intro i

fin_cases i <;> simp [c]

have hc1 : ∀ i : Fin 2, c i ≤ 1 := by

intro i

fin_cases i <;> simp [c]

have hcnorm : ∑ i : Fin 2, (c i)^2 = 1 := by

simp [c, Fin.sum_univ_two]

have heq : ∑ i : Fin 2, f (c i) = 1 := hf_norm 2 (by norm_num) c hcnn hc1 hcnorm

simp [c, Fin.sum_univ_two, hf1] at heq

linarith

lemma f_lt_one_of_lt_one (f : ℝ → ℝ) (hm : SatisfiesMultiplicativity f) (hf1 : f 1 = 1)

(hf_cont : ContinuousOn f (Set.Icc 0 1))

(hf0 : f 0 = 0)

(x : ℝ) (hx0 : 0 < x) (hx1 : x < 1) : f x < 1 := by

by_contra h_lt

have h_ge : 1 ≤ f x := le_of_not_gt h_lt

have h_pow_ge : ∀ n : ℕ, 1 ≤ f (x ^ n) := by

intro n

rw [mul_pow_eq f hm hf1 n x hx0.le hx1.le]

exact one_le_pow₀ h_ge

have hx_pow_zero : Tendsto (fun n : ℕ => x ^ n) atTop (nhds 0) :=

tendsto_pow_atTop_nhds_zero_of_lt_one hx0.le hx1

have hx_pow_within : Tendsto (fun n : ℕ => x ^ n) atTop (nhdsWithin 0 (Set.Icc 0 1)) := by

refine tendsto_nhdsWithin_iff.mpr ?_

refine ⟨hx_pow_zero, Filter.Eventually.of_forall ?_⟩

intro n

exact ⟨pow_nonneg hx0.le n, pow_le_one₀ hx0.le hx1.le⟩

have hzero_mem : (0 : ℝ) ∈ Set.Icc 0 1 := ⟨le_rfl, by norm_num⟩

have hcont0 : ContinuousWithinAt f (Set.Icc 0 1) 0 := by

simpa using hf_cont (x := 0) hzero_mem