From a60b092cfff64a505ed4b902797faf10bcfdaaa0 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Mon, 11 May 2026 22:10:42 -0500 Subject: [PATCH] Track EigenGate dependency slice --- .../Semantics/Core/FoldedPointManifold.lean | 409 ++++++++++++++++++ .../Core/PathEpigeneticManifold.lean | 282 ++++++++++++ .../Semantics/Core/QuantumFoamBoundary.lean | 92 ++++ .../Core/S3CProjectedGeodesicResolution.lean | 245 +++++++++++ .../Semantics/Core/UnderverseZeroLayer.lean | 101 +++++ .../Semantics/Semantics/Kernel/EigenGate.lean | 180 ++++++++ .../Semantics/Semantics/Kernel/GateChain.lean | 56 +++ .../Semantics/Testing/ErdosSurface.lean | 149 +++++++ 8 files changed, 1514 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Core/FoldedPointManifold.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Core/PathEpigeneticManifold.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Core/QuantumFoamBoundary.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Core/S3CProjectedGeodesicResolution.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Core/UnderverseZeroLayer.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Kernel/EigenGate.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Kernel/GateChain.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Testing/ErdosSurface.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Core/FoldedPointManifold.lean b/0-Core-Formalism/lean/Semantics/Semantics/Core/FoldedPointManifold.lean new file mode 100644 index 00000000..b8942041 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Core/FoldedPointManifold.lean @@ -0,0 +1,409 @@ +/- +FoldedPointManifold.lean — apparent 0D footprint with higher-dimensional interior + +This module makes explicit the frame distinction: + + observer-resolved dimension = 0 + internal/folded dimension may be > 0 + +That prevents the model from treating "0D" as automatically empty. A point may +be an observer-frame footprint of folded higher-dimensional structure, but the +claim is admitted only when neutral closure, replay, bounded dimensionality, and +torsional potential are declared. + +The stronger loopback claim is separate: when the observer frame has lost all +resolution at apparent 0D, a declared 16D interior may become a permeable return +surface only if the permeability witness is present. + +Permeability is not free leakage. It is conservation-preserving porosity: every +dimensional level that participates in the loopback must carry the same +accounting value. +-/ + +import Semantics.FixedPoint + +namespace Semantics.FoldedPointManifold + +open Semantics.FixedPoint + +/-- Terminal gate for a folded-point claim. -/ +inductive FoldDecision where + | admit + | hold + | reject + deriving Repr, BEq, DecidableEq + +/-- Terminal gate for the 0D -> 16D loopback/permeability claim. -/ +inductive LoopbackDecision where + | loopback + | hold + | reject + deriving Repr, BEq, DecidableEq + +/-- Terminal gate for conservation across the dimensional ladder. -/ +inductive ConservationDecision where + | conserved + | hold + | reject + deriving Repr, BEq, DecidableEq + +/-- Minimal folded-point event. + +`resolvedDim = 0` means the observer frame sees no extension. +`internalDim > 0` means the event carries folded interior degrees of freedom. +`neutralClosure` links the claim back to U0 accounting. +`torsionPotential` is normalized Q0.16 expression potential. +`permeabilityDeclared` is the extra witness for the stronger loopback claim. +-/ +structure FoldedPointEvent where + resolvedDim : Nat + internalDim : Nat + apparentPoint : Bool + neutralClosure : Bool + replayReceiptPresent : Bool + torsionPotential : Q0_16 + permeabilityDeclared : Bool + deriving Repr, BEq, DecidableEq + +/-- A folded point is a point only in the observer frame. -/ +def isFoldedPoint (e : FoldedPointEvent) : Bool := + e.apparentPoint && e.resolvedDim == 0 && e.internalDim > 0 + +/-- Current model cap: the folded interior may be up to the declared 16D +manifold, but not an unbounded free variable. -/ +def withinDeclaredDimensionalCap (e : FoldedPointEvent) : Bool := + e.internalDim <= 16 + +/-- There must be nonzero torsional potential to unfold. -/ +def hasTorsionPotential (e : FoldedPointEvent) : Bool := + e.torsionPotential.val != 0 + +/-- The observer frame has lost all spatial resolution at the footprint. -/ +def resolutionLost (e : FoldedPointEvent) : Bool := + e.apparentPoint && e.resolvedDim == 0 + +/-- A folded point is admissible only when the apparent point, internal +dimensional witness, neutral closure, replay, cap, and torsion potential close. +Missing replay/neutrality/capacity routes to HOLD if the event is at least a +folded-point candidate. Non-folded points reject the folded-space claim. -/ +def decideFoldedPoint (e : FoldedPointEvent) : FoldDecision := + if isFoldedPoint e then + if withinDeclaredDimensionalCap e && + e.neutralClosure && + e.replayReceiptPresent && + hasTorsionPotential e then + .admit + else + .hold + else + .reject + +/-- The stronger cyclic claim: after apparent 0D, a declared 16D interior can +be treated as a permeable return surface only when the separate permeability +witness is present. -/ +def decideLoopback (e : FoldedPointEvent) : LoopbackDecision := + if resolutionLost e then + if e.internalDim == 16 && + e.permeabilityDeclared && + e.neutralClosure && + e.replayReceiptPresent && + hasTorsionPotential e then + .loopback + else + .hold + else + .reject + +/-- Conservation witness across the compressed 0D seed, carrier path, generator, +projection surface, and 16D expression space. + +`mengerZeroSeed` marks the 0D boundary as a porous/fractal conservation limit, +not an empty point. The values are abstract accounting charges/loads, not +physical mass claims. +-/ +structure DimensionalConservation where + level0 : Int + level1 : Int + level4 : Int + level3 : Int + level16 : Int + mengerZeroSeed : Bool + replayReceiptPresent : Bool + deriving Repr, BEq, DecidableEq + +/-- Conservation means every declared dimensional level carries the same +accounting value. -/ +def conservedAcrossLevels (c : DimensionalConservation) : Bool := + c.level0 == c.level1 && + c.level1 == c.level4 && + c.level4 == c.level3 && + c.level3 == c.level16 + +/-- The Menger-style 0D seed only admits conservation when replay is present. +Broken conservation rejects. A missing porous seed or replay is HOLD. -/ +def decideConservation (c : DimensionalConservation) : ConservationDecision := + if conservedAcrossLevels c then + if c.mengerZeroSeed && c.replayReceiptPresent then .conserved + else .hold + else + .reject + +/-- Canonical fixture: observer sees 0D, interior declares 16D, closure and +replay are present, and torsional potential can unfold. -/ +def folded16Fixture : FoldedPointEvent := + { resolvedDim := 0 + , internalDim := 16 + , apparentPoint := true + , neutralClosure := true + , replayReceiptPresent := true + , torsionPotential := Q0_16.half + , permeabilityDeclared := true } + +/-- Same folded candidate, but no replay receipt: HOLD, not ADMIT. -/ +def missingReplayFixture : FoldedPointEvent := + { folded16Fixture with replayReceiptPresent := false } + +/-- Same observer point, but internal dimensionality exceeds the declared cap: +HOLD until a new cap/law is declared. -/ +def overCapFixture : FoldedPointEvent := + { folded16Fixture with internalDim := 17 } + +/-- An ordinary 0D point with no internal dimension rejects a folded-space +claim. -/ +def ordinaryPointFixture : FoldedPointEvent := + { folded16Fixture with internalDim := 0 } + +/-- Folded and neutral, but no permeability witness: HOLD for loopback. -/ +def noPermeabilityFixture : FoldedPointEvent := + { folded16Fixture with permeabilityDeclared := false } + +/-- Menger-style 0D seed preserves the same accounting value across every +declared dimensional level. -/ +def mengerConservedFixture : DimensionalConservation := + { level0 := 3 + , level1 := 3 + , level4 := 3 + , level3 := 3 + , level16 := 3 + , mengerZeroSeed := true + , replayReceiptPresent := true } + +def brokenConservationFixture : DimensionalConservation := + { mengerConservedFixture with level16 := 4 } + +def missingMengerSeedFixture : DimensionalConservation := + { mengerConservedFixture with mengerZeroSeed := false } + +/-! ## Gate Algebra for Total Interaction + +The total interaction is a pair `I_total(s) = (Γ(s), ΔR(s))`. + +`Γ(s)` is the ordered tensor product of individual gate outcomes. +The order is: REJECT > HOLD > ADMIT. + +`ΔR(s)` is the resolution delta: shortcut gain plus shell error recovery +minus projected error. +-/ + +/-- Ordered gate outcomes for the tensor product. + REJECT > HOLD > ADMIT - this ordering ensures that a single + rejection dominates, and a single hold blocks admission. -/ +inductive GateOutcome where + | reject + | hold + | admit + deriving Repr, BEq, DecidableEq + +/-- Ordered tensor product (⊗) of gate outcomes. + If any gate rejects, the product rejects. + If any gate holds (and none reject), the product holds. + Only if all gates admit does the product admit. -/ +def gateCompose (g1 g2 : GateOutcome) : GateOutcome := + match g1 with + | .reject => .reject + | .hold => match g2 with | .reject => .reject | _ => .hold + | .admit => g2 + +/-- The tensor product extends to a list of gates. -/ +def gateComposeList (gs : List GateOutcome) : GateOutcome := + gs.foldl gateCompose .admit + +/-- Resolution delta components for the 0D→16D throat shortcut. -/ +structure ResolutionDelta where + manifoldDistance : Int -- D_m: full manifold traversal distance + throatDistance : Int -- D_t: shortcut throat distance + shellError : Int -- E_s: recoverable shell baseline error + projectedError : Int -- E_p: new residual from the projection + deriving Repr, BEq, DecidableEq + +/-- Compute the net resolution change. + Positive = improvement (throat saves more than projection costs). + Zero = break-even. + Negative = decreased resolution. -/ +def deltaResolution (r : ResolutionDelta) : Int := + (r.manifoldDistance - r.throatDistance) + r.shellError - r.projectedError + +/-- Final interaction outcome after applying the decision law. -/ +inductive InteractionOutcome where + | improved -- Γ = ADMIT and ΔR > 0 + | unchanged -- Γ = ADMIT and ΔR = 0 + | decreased -- Γ = ADMIT and ΔR < 0 + | hold -- Γ = HOLD + | reject -- Γ = REJECT + deriving Repr, BEq, DecidableEq + +/-- The total interaction pair: (gate tensor, resolution delta). -/ +structure TotalInteraction where + gateTensor : GateOutcome + deltaR : ResolutionDelta + deriving Repr + +/-- Apply the decision law to the total interaction pair. + If Γ = REJECT → REJECT + If Γ = HOLD → HOLD + If Γ = ADMIT → sign(ΔR) determines IMPROVED/UNCHANGED/DECREASED -/ +def interact (ti : TotalInteraction) : InteractionOutcome := + match ti.gateTensor with + | .reject => .reject + | .hold => .hold + | .admit => + let d := deltaResolution ti.deltaR + if d > 0 then .improved + else if d == 0 then .unchanged + else .decreased + +/-- Canonical gate tensor: all five gates admit. -/ +def allAdmit : GateOutcome := .admit + +/-- Fixture: the throat saves distance and shell error exceeds projection cost. -/ +def positiveDeltaFixture : ResolutionDelta := + { manifoldDistance := 10 + , throatDistance := 3 + , shellError := 2 + , projectedError := 1 } + +/-- Fixture: the throat costs more than it saves. -/ +def negativeDeltaFixture : ResolutionDelta := + { positiveDeltaFixture with throatDistance := 15, projectedError := 5 } + +/-- Fixture: break-even. -/ +def zeroDeltaFixture : ResolutionDelta := + { positiveDeltaFixture with throatDistance := 11, projectedError := 1 } + +/-- Total interaction with all gates open and positive delta → improved. -/ +def improvedInteractionFixture : TotalInteraction := + { gateTensor := allAdmit, deltaR := positiveDeltaFixture } + +/-- Total interaction with all gates open and negative delta → decreased. -/ +def decreasedInteractionFixture : TotalInteraction := + { gateTensor := allAdmit, deltaR := negativeDeltaFixture } + +/-- Total interaction with a reject in the gate tensor → reject. -/ +def rejectedInteractionFixture : TotalInteraction := + { gateTensor := .reject, deltaR := positiveDeltaFixture } + +/-- Total interaction with a hold in the gate tensor → hold (ΔR ignored). -/ +def heldInteractionFixture : TotalInteraction := + { gateTensor := .hold, deltaR := positiveDeltaFixture } + +theorem improvedFixture_yields_improved : + interact improvedInteractionFixture = .improved := by + native_decide + +theorem decreasedFixture_yields_decreased : + interact decreasedInteractionFixture = .decreased := by + native_decide + +theorem rejectedFixture_yields_reject : + interact rejectedInteractionFixture = .reject := by + native_decide + +theorem heldFixture_yields_hold : + interact heldInteractionFixture = .hold := by + native_decide + +theorem gateCompose_reject_dominates_left : + gateCompose .reject .admit = .reject := by rfl + +theorem gateCompose_reject_dominates_right : + gateCompose .admit .reject = .reject := by rfl + +theorem gateCompose_hold_blocks_admit : + gateCompose .hold .admit = .hold := by rfl + +theorem gateCompose_admit_neutral : + gateCompose .admit .admit = .admit := by rfl + +theorem deltaResolution_positive_fixture : + deltaResolution positiveDeltaFixture = 8 := by native_decide + +theorem deltaResolution_negative_fixture : + deltaResolution negativeDeltaFixture = -8 := by native_decide + +theorem deltaResolution_zero_fixture : + deltaResolution zeroDeltaFixture = 0 := by native_decide + +theorem folded16Fixture_admits : + decideFoldedPoint folded16Fixture = .admit := by + native_decide + +theorem missingReplayFixture_holds : + decideFoldedPoint missingReplayFixture = .hold := by + native_decide + +theorem overCapFixture_holds : + decideFoldedPoint overCapFixture = .hold := by + native_decide + +theorem ordinaryPointFixture_rejects : + decideFoldedPoint ordinaryPointFixture = .reject := by + native_decide + +theorem folded16Fixture_loopsBack : + decideLoopback folded16Fixture = .loopback := by + native_decide + +theorem noPermeabilityFixture_holdsLoopback : + decideLoopback noPermeabilityFixture = .hold := by + native_decide + +theorem ordinaryPointFixture_holdsLoopback : + decideLoopback ordinaryPointFixture = .hold := by + native_decide + +theorem mengerConservedFixture_conserved : + decideConservation mengerConservedFixture = .conserved := by + native_decide + +theorem brokenConservationFixture_rejects : + decideConservation brokenConservationFixture = .reject := by + native_decide + +theorem missingMengerSeedFixture_holds : + decideConservation missingMengerSeedFixture = .hold := by + native_decide + +#eval isFoldedPoint folded16Fixture +#eval decideFoldedPoint folded16Fixture +#eval decideFoldedPoint missingReplayFixture +#eval decideFoldedPoint ordinaryPointFixture +#eval decideLoopback folded16Fixture +#eval decideLoopback noPermeabilityFixture +#eval decideConservation mengerConservedFixture +#eval decideConservation brokenConservationFixture + +#eval gateCompose .reject .admit +#eval gateCompose .hold .admit +#eval gateCompose .admit .admit +#eval gateComposeList [.admit, .admit, .admit] +#eval gateComposeList [.admit, .hold, .admit] +#eval gateComposeList [.admit, .reject, .admit] +#eval deltaResolution positiveDeltaFixture +#eval deltaResolution negativeDeltaFixture +#eval deltaResolution zeroDeltaFixture +#eval interact improvedInteractionFixture +#eval interact decreasedInteractionFixture +#eval interact rejectedInteractionFixture +#eval interact heldInteractionFixture + +end Semantics.FoldedPointManifold diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Core/PathEpigeneticManifold.lean b/0-Core-Formalism/lean/Semantics/Semantics/Core/PathEpigeneticManifold.lean new file mode 100644 index 00000000..271999f1 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Core/PathEpigeneticManifold.lean @@ -0,0 +1,282 @@ +/- +PathEpigeneticManifold.lean — 1D regulatory path over a 16D manifold + +This module models the "circuit path as epigenetic control strand" idea: +the 1D path is stable carrier geometry, while finite regulatory marks on that +path determine which dimensions of a 16D manifold are expressed, damped, +receipted, or routed to quarantine. + +The claim boundary is intentionally narrow. This is not a biological +equivalence, fabrication rule, or compression claim. It is a receipt-bearing +state update law. +-/ + +import Semantics.FixedPoint + +namespace Semantics.PathEpigeneticManifold + +open Semantics.FixedPoint + +/-- The 16 addressable dimensions of the manifold packet. -/ +inductive Dim16 where + | identity + | route + | scale + | phase + | torsion + | curvature + | energy + | velocity + | residual + | semanticMass + | confidence + | density + | topology + | witness + | underverse + | time + deriving Repr, BEq, DecidableEq + +/-- Finite regulatory mark actions carried by a 1D path site. -/ +inductive MarkerAction where + | activate + | damp + | gateWitness + | quarantine + deriving Repr, BEq, DecidableEq + +/-- Terminal decision for a path-regulated manifold update. -/ +inductive PathDecision where + | admit + | hold + | quarantine + deriving Repr, BEq, DecidableEq + +/-- One regulatory marker attached to a path site. -/ +structure RegulatoryMarker where + target : Dim16 + action : MarkerAction + strength : Q0_16 + receiptPresent : Bool + deriving Repr, BEq, DecidableEq + +/-- One 1D carrier-site. `layoutClear` is the circuit/route design-rule gate. -/ +structure PathSite where + siteId : UInt16 + marker : RegulatoryMarker + layoutClear : Bool + deriving Repr, BEq, DecidableEq + +/-- The 16D manifold state. All fields use Q0.16 because they are normalized +dimensionless expression levels in this first receipt surface. -/ +structure Manifold16 where + identity : Q0_16 + route : Q0_16 + scale : Q0_16 + phase : Q0_16 + torsion : Q0_16 + curvature : Q0_16 + energy : Q0_16 + velocity : Q0_16 + residual : Q0_16 + semanticMass : Q0_16 + confidence : Q0_16 + density : Q0_16 + topology : Q0_16 + witness : Q0_16 + underverse : Q0_16 + time : Q0_16 + deriving Repr, BEq, DecidableEq + +namespace Manifold16 + +def zero : Manifold16 := + { identity := Q0_16.zero + , route := Q0_16.zero + , scale := Q0_16.zero + , phase := Q0_16.zero + , torsion := Q0_16.zero + , curvature := Q0_16.zero + , energy := Q0_16.zero + , velocity := Q0_16.zero + , residual := Q0_16.zero + , semanticMass := Q0_16.zero + , confidence := Q0_16.zero + , density := Q0_16.zero + , topology := Q0_16.zero + , witness := Q0_16.zero + , underverse := Q0_16.zero + , time := Q0_16.zero } + +def get (s : Manifold16) : Dim16 → Q0_16 + | Dim16.identity => s.identity + | Dim16.route => s.route + | Dim16.scale => s.scale + | Dim16.phase => s.phase + | Dim16.torsion => s.torsion + | Dim16.curvature => s.curvature + | Dim16.energy => s.energy + | Dim16.velocity => s.velocity + | Dim16.residual => s.residual + | Dim16.semanticMass => s.semanticMass + | Dim16.confidence => s.confidence + | Dim16.density => s.density + | Dim16.topology => s.topology + | Dim16.witness => s.witness + | Dim16.underverse => s.underverse + | Dim16.time => s.time + +def set (s : Manifold16) (d : Dim16) (v : Q0_16) : Manifold16 := + match d with + | Dim16.identity => { s with identity := v } + | Dim16.route => { s with route := v } + | Dim16.scale => { s with scale := v } + | Dim16.phase => { s with phase := v } + | Dim16.torsion => { s with torsion := v } + | Dim16.curvature => { s with curvature := v } + | Dim16.energy => { s with energy := v } + | Dim16.velocity => { s with velocity := v } + | Dim16.residual => { s with residual := v } + | Dim16.semanticMass => { s with semanticMass := v } + | Dim16.confidence => { s with confidence := v } + | Dim16.density => { s with density := v } + | Dim16.topology => { s with topology := v } + | Dim16.witness => { s with witness := v } + | Dim16.underverse => { s with underverse := v } + | Dim16.time => { s with time := v } + +end Manifold16 + +/-- A regulatory marker is admissible only if its local layout and receipt close. -/ +def markerAdmissible (site : PathSite) : Bool := + site.layoutClear && site.marker.receiptPresent + +/-- Apply one marker. Missing receipt leaves the manifold unchanged; the decision +gate records HOLD separately. Layout failure routes to quarantine. -/ +def applyMarker (s : Manifold16) (site : PathSite) : Manifold16 := + if !site.layoutClear then + (s.set Dim16.underverse site.marker.strength).set Dim16.residual site.marker.strength + else if !site.marker.receiptPresent then + s + else + match site.marker.action with + | MarkerAction.activate => + s.set site.marker.target site.marker.strength + | MarkerAction.damp => + s.set site.marker.target Q0_16.zero + | MarkerAction.gateWitness => + s.set Dim16.witness Q0_16.one + | MarkerAction.quarantine => + (s.set Dim16.underverse site.marker.strength).set Dim16.residual site.marker.strength + +/-- Fold a 1D path over the 16D manifold. -/ +def applyPath (s : Manifold16) (path : List PathSite) : Manifold16 := + path.foldl applyMarker s + +def anyLayoutViolation : List PathSite → Bool + | [] => false + | site :: rest => (!site.layoutClear) || anyLayoutViolation rest + +def anyMissingReceipt : List PathSite → Bool + | [] => false + | site :: rest => (site.layoutClear && !site.marker.receiptPresent) || anyMissingReceipt rest + +def anyQuarantineMarker : List PathSite → Bool + | [] => false + | site :: rest => (site.marker.action == MarkerAction.quarantine && site.marker.receiptPresent) || anyQuarantineMarker rest + +/-- Path-level decision: physical/layout violation or explicit quarantine wins; +otherwise missing receipts HOLD; fully receipted paths ADMIT. -/ +def decidePath (path : List PathSite) : PathDecision := + if anyLayoutViolation path || anyQuarantineMarker path then .quarantine + else if anyMissingReceipt path then .hold + else .admit + +/-- One completed path-regulated update receipt. -/ +structure PathReceipt where + before : Manifold16 + after : Manifold16 + siteCount : Nat + decision : PathDecision + deriving Repr, BEq, DecidableEq + +def runPath (s : Manifold16) (path : List PathSite) : PathReceipt := + { before := s + , after := applyPath s path + , siteCount := path.length + , decision := decidePath path } + +def qSmall : Q0_16 := ⟨1⟩ +def qMedium : Q0_16 := ⟨0x0100⟩ + +def torsionSite : PathSite := + { siteId := 0 + , marker := + { target := Dim16.torsion + , action := MarkerAction.activate + , strength := qMedium + , receiptPresent := true } + , layoutClear := true } + +def dampResidualSite : PathSite := + { siteId := 1 + , marker := + { target := Dim16.residual + , action := MarkerAction.damp + , strength := qSmall + , receiptPresent := true } + , layoutClear := true } + +def witnessSite : PathSite := + { siteId := 2 + , marker := + { target := Dim16.witness + , action := MarkerAction.gateWitness + , strength := Q0_16.one + , receiptPresent := true } + , layoutClear := true } + +def missingReceiptSite : PathSite := + { torsionSite with marker := { torsionSite.marker with receiptPresent := false } } + +def layoutViolationSite : PathSite := + { torsionSite with layoutClear := false } + +def admittedPath : List PathSite := [torsionSite, witnessSite] +def holdPath : List PathSite := [missingReceiptSite] +def quarantinePath : List PathSite := [layoutViolationSite] + +theorem admittedPathActivatesTorsion : + (runPath Manifold16.zero admittedPath).after.torsion = qMedium := by + native_decide + +theorem admittedPathClosesWitness : + (runPath Manifold16.zero admittedPath).after.witness = Q0_16.one := by + native_decide + +theorem admittedPathDecision : + (runPath Manifold16.zero admittedPath).decision = .admit := by + native_decide + +theorem holdPathLeavesTorsionUnchanged : + (runPath Manifold16.zero holdPath).after.torsion = Q0_16.zero := by + native_decide + +theorem holdPathDecision : + (runPath Manifold16.zero holdPath).decision = .hold := by + native_decide + +theorem quarantinePathRoutesResidual : + (runPath Manifold16.zero quarantinePath).after.residual = qMedium := by + native_decide + +theorem quarantinePathDecision : + (runPath Manifold16.zero quarantinePath).decision = .quarantine := by + native_decide + +#eval (runPath Manifold16.zero admittedPath).decision +#eval (runPath Manifold16.zero admittedPath).after.torsion +#eval (runPath Manifold16.zero holdPath).decision +#eval (runPath Manifold16.zero quarantinePath).after.underverse + +end Semantics.PathEpigeneticManifold diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Core/QuantumFoamBoundary.lean b/0-Core-Formalism/lean/Semantics/Semantics/Core/QuantumFoamBoundary.lean new file mode 100644 index 00000000..cf862a13 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Core/QuantumFoamBoundary.lean @@ -0,0 +1,92 @@ +/- +QuantumFoamBoundary.lean — bounded fluctuation guard around U0 + +Quantum foam is modeled here as an accounting boundary around the zero layer, +not as a promotion rule. Exact neutral closure still belongs to U0. Foam only +classifies sub-resolution, unreceipted, or stochastic jitter as HOLD. +-/ + +namespace Semantics.QuantumFoamBoundary + +/-- Coarse scale band for an accounting fluctuation. -/ +inductive FoamScale where + | deterministic + | measurementFloor + | planckAnalogy + | subResolution + deriving Repr, BEq, DecidableEq + +/-- Decision emitted by the foam boundary. -/ +inductive FoamDecision where + | exactClosure + | holdFoam + | rejectClaim + deriving Repr, BEq, DecidableEq + +/-- Minimal foam-boundary sample. + +`netCharge` is the recomputed visible + Underverse + sink charge. +`jitterBound` is the declared symmetric tolerance for a measurement/noise floor. +`replayReceiptPresent` distinguishes exact U0 closure from a balanced-looking +but unreceipted claim. +-/ +structure FoamSample where + scale : FoamScale + netCharge : Int + jitterBound : Nat + replayReceiptPresent : Bool + deriving Repr, BEq, DecidableEq + +/-- A signed integer lies inside the declared symmetric jitter band. -/ +def withinJitter (s : FoamSample) : Bool := + s.netCharge.natAbs <= s.jitterBound + +/-- Foam boundary classifier. + +Exact zero with replay belongs to `exactClosure`. +Nonzero values inside a declared jitter band are HOLD, never ADMIT. +Nonzero values outside the band reject the zero/foam claim. +-/ +def decideFoamBoundary (s : FoamSample) : FoamDecision := + if s.netCharge == 0 && s.replayReceiptPresent then .exactClosure + else if withinJitter s then .holdFoam + else .rejectClaim + +def exactZeroFixture : FoamSample := + { scale := .deterministic + , netCharge := 0 + , jitterBound := 0 + , replayReceiptPresent := true + } + +def foamJitterFixture : FoamSample := + { scale := .subResolution + , netCharge := 1 + , jitterBound := 2 + , replayReceiptPresent := false + } + +def outOfBandFixture : FoamSample := + { scale := .measurementFloor + , netCharge := 5 + , jitterBound := 2 + , replayReceiptPresent := false + } + +theorem exactZeroFixture_closes : + decideFoamBoundary exactZeroFixture = .exactClosure := by + rfl + +theorem foamJitterFixture_holds : + decideFoamBoundary foamJitterFixture = .holdFoam := by + rfl + +theorem outOfBandFixture_rejects : + decideFoamBoundary outOfBandFixture = .rejectClaim := by + rfl + +#eval decideFoamBoundary exactZeroFixture +#eval decideFoamBoundary foamJitterFixture +#eval decideFoamBoundary outOfBandFixture + +end Semantics.QuantumFoamBoundary diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Core/S3CProjectedGeodesicResolution.lean b/0-Core-Formalism/lean/Semantics/Semantics/Core/S3CProjectedGeodesicResolution.lean new file mode 100644 index 00000000..de24ec79 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Core/S3CProjectedGeodesicResolution.lean @@ -0,0 +1,245 @@ +/- +S3CProjectedGeodesicResolution.lean — folded-throat resolution gate + +This module compares the old S3C projected-geodesic score against the refined +folded-point theory: + + baseline S3C score + = manifold distance minus shell/projection error + + folded-throat score + = baseline distance plus throat shortcut gain minus projected error + +The refinement is allowed to improve resolution only when the 0D throat has a +declared folded 16D interior, loopback permeability, Menger-style conservation, +and genus-3/S3C lobe alignment. Otherwise the refinement holds or rejects +instead of silently increasing precision. +-/ + +import Semantics.Core.FoldedPointManifold + +namespace Semantics.S3CProjectedGeodesicResolution + +open Semantics.FoldedPointManifold + +/-- Resolution comparison after applying the folded-throat refinement. -/ +inductive ResolutionDecision where + | improved + | unchanged + | decreased + | hold + | reject + deriving Repr, BEq, DecidableEq + +/-- Diagnostic reason for the resolution decision. -/ +inductive ResolutionReason where + | foldedPointRejected + | loopbackRejected + | conservationRejected + | foldedPointMissing + | loopbackMissing + | conservationMissing + | lobeMismatch + | noThroatShortcut + | shortcutOutrunsResidual + | residualOutrunsShortcut + | exactBoundary + deriving Repr, BEq, DecidableEq + +/-- Minimal finite S3C geodesic sample. + +`manifoldDist` is the original S3C route distance. +`throatLength` is the route through the projected 0D throat. +`shellError` is the old shell/projection residual. +`projectedError` is the residual after the folded-throat projection. +`lobeCount = 3` is the S3C/genus-3 alignment witness. +-/ +structure S3CGeodesicSample where + manifoldDist : Nat + throatLength : Nat + shellError : Nat + projectedError : Nat + lobeCount : Nat + folded : FoldedPointEvent + conservation : DimensionalConservation + deriving Repr, BEq, DecidableEq + +/-- Old resolution score: larger means more usable route resolution. -/ +def baselineScore (s : S3CGeodesicSample) : Nat := + s.manifoldDist - s.shellError + +/-- Distance saved by going through the projected throat. -/ +def shortcutGain (s : S3CGeodesicSample) : Nat := + s.manifoldDist - s.throatLength + +/-- S3C's three-handle/lobe alignment gate. -/ +def genus3Aligned (s : S3CGeodesicSample) : Bool := + s.lobeCount == 3 + +/-- Full admissibility gate for using the folded 0D throat as a precision +refinement. -/ +def foldedThroatAdmissible (s : S3CGeodesicSample) : Bool := + decideFoldedPoint s.folded == .admit && + decideLoopback s.folded == .loopback && + decideConservation s.conservation == .conserved && + genus3Aligned s && + s.throatLength <= s.manifoldDist + +/-- Refined resolution score. + +The refinement can only claim a sharper route when the folded-throat gate is +closed. Otherwise it preserves the baseline score and lets `decideResolution` +return HOLD/REJECT where appropriate. +-/ +def refinedScore (s : S3CGeodesicSample) : Nat := + if foldedThroatAdmissible s then + s.manifoldDist + shortcutGain s - s.projectedError + else + baselineScore s + +/-- Amount of old uncertainty that the folded-throat refinement can pay down. + +The refinement can improve only when this budget is larger than the new +projected residual: + + shortcutGain + shellError > projectedError +-/ +def resolutionBudget (s : S3CGeodesicSample) : Nat := + shortcutGain s + s.shellError + +/-- Signed score delta: refined score minus baseline score. -/ +def resolutionDelta (s : S3CGeodesicSample) : Int := + Int.ofNat (refinedScore s) - Int.ofNat (baselineScore s) + +/-- Compare the baseline and refined scores. -/ +def compareScores (base refined : Nat) : ResolutionDecision := + if refined > base then .improved + else if refined == base then .unchanged + else .decreased + +/-- Decide whether the folded-throat theory improves, preserves, decreases, or +refuses the projected-geodesic resolution. -/ +def decideResolution (s : S3CGeodesicSample) : ResolutionDecision := + if decideFoldedPoint s.folded == .reject || + decideLoopback s.folded == .reject || + decideConservation s.conservation == .reject then + .reject + else if foldedThroatAdmissible s then + compareScores (baselineScore s) (refinedScore s) + else + .hold + +/-- Explain why the score improved, decreased, held, or rejected. -/ +def explainResolution (s : S3CGeodesicSample) : ResolutionReason := + if decideFoldedPoint s.folded == .reject then + .foldedPointRejected + else if decideLoopback s.folded == .reject then + .loopbackRejected + else if decideConservation s.conservation == .reject then + .conservationRejected + else if decideFoldedPoint s.folded != .admit then + .foldedPointMissing + else if decideLoopback s.folded != .loopback then + .loopbackMissing + else if decideConservation s.conservation != .conserved then + .conservationMissing + else if !genus3Aligned s then + .lobeMismatch + else if !(s.throatLength <= s.manifoldDist) then + .noThroatShortcut + else + match compareScores (baselineScore s) (refinedScore s) with + | .improved => .shortcutOutrunsResidual + | .decreased => .residualOutrunsShortcut + | .unchanged => .exactBoundary + | .hold => .exactBoundary + | .reject => .exactBoundary + +/-- The theory improves resolution when the throat is short, projection error is +lower than the old shell residual, and all folded/conservation gates close. -/ +def improvedFixture : S3CGeodesicSample := + { manifoldDist := 100 + , throatLength := 40 + , shellError := 20 + , projectedError := 5 + , lobeCount := 3 + , folded := folded16Fixture + , conservation := mengerConservedFixture } + +/-- The theory can decrease resolution when a nominally admissible throat adds +too little shortcut gain and the projected residual is worse. -/ +def decreasedFixture : S3CGeodesicSample := + { improvedFixture with + throatLength := 95 + shellError := 10 + projectedError := 20 } + +/-- Missing permeability leaves the refinement in HOLD. -/ +def holdFixture : S3CGeodesicSample := + { improvedFixture with folded := noPermeabilityFixture } + +/-- Broken conservation rejects the refined geodesic claim. -/ +def rejectFixture : S3CGeodesicSample := + { improvedFixture with conservation := brokenConservationFixture } + +/-- The exact boundary where folded-throat gain equals projected residual. -/ +def unchangedFixture : S3CGeodesicSample := + { improvedFixture with + throatLength := 90 + shellError := 10 + projectedError := 20 } + +theorem improvedFixtureImproves : + decideResolution improvedFixture = .improved := by + native_decide + +theorem decreasedFixtureDecreases : + decideResolution decreasedFixture = .decreased := by + native_decide + +theorem holdFixtureHolds : + decideResolution holdFixture = .hold := by + native_decide + +theorem rejectFixtureRejects : + decideResolution rejectFixture = .reject := by + native_decide + +theorem unchangedFixtureUnchanged : + decideResolution unchangedFixture = .unchanged := by + native_decide + +theorem improvedFixtureBaselineScore : + baselineScore improvedFixture = 80 := by + native_decide + +theorem improvedFixtureRefinedScore : + refinedScore improvedFixture = 155 := by + native_decide + +theorem improvedFixtureReason : + explainResolution improvedFixture = .shortcutOutrunsResidual := by + native_decide + +theorem decreasedFixtureReason : + explainResolution decreasedFixture = .residualOutrunsShortcut := by + native_decide + +theorem unchangedFixtureReason : + explainResolution unchangedFixture = .exactBoundary := by + native_decide + +#eval baselineScore improvedFixture +#eval refinedScore improvedFixture +#eval resolutionBudget improvedFixture +#eval resolutionDelta improvedFixture +#eval decideResolution improvedFixture +#eval explainResolution improvedFixture +#eval decideResolution decreasedFixture +#eval explainResolution decreasedFixture +#eval decideResolution unchangedFixture +#eval explainResolution unchangedFixture +#eval decideResolution holdFixture +#eval decideResolution rejectFixture + +end Semantics.S3CProjectedGeodesicResolution diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Core/UnderverseZeroLayer.lean b/0-Core-Formalism/lean/Semantics/Semantics/Core/UnderverseZeroLayer.lean new file mode 100644 index 00000000..e79db15b --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Core/UnderverseZeroLayer.lean @@ -0,0 +1,101 @@ +/- +UnderverseZeroLayer.lean — explicit neutral closure accounting + +The zero layer is the receipt boundary between observable accounting and +Underverse/complement accounting. It prevents "missing" or "opposite" terms +from becoming free variables: a neutral event is admitted only when the net +charge closes exactly and the replay receipt is present. + +The genus-3 case is deliberately a checked assumption surface, not a topology +proof. Genus 3 may be the selected chart, but zero charge still has to be +declared and replayed. +-/ + +namespace Semantics.UnderverseZeroLayer + +/-- Which chart the neutral event is being checked in. -/ +inductive ChargeChart where + | ordinary + | genus3 + | mirror + | antiBaryonic + deriving Repr, BEq, DecidableEq + +/-- Terminal decision for the zero layer. -/ +inductive ZeroDecision where + | admit + | hold + | reject + deriving Repr, BEq, DecidableEq + +/-- Minimal zero-layer event. + +`observableCharge` is the visible/accounted side. +`underverseCharge` is the complement, inverse, hidden, or Underverse side. +`sinkCharge` is a typed loss/annihilation/sink sidecar. + +The event is neutral only when all three sum to zero and replay is present. +-/ +structure ZeroLayerEvent where + chart : ChargeChart + genus : Nat + observableCharge : Int + underverseCharge : Int + sinkCharge : Int + replayReceiptPresent : Bool + deriving Repr, BEq, DecidableEq + +/-- Net accounting charge across observable, Underverse, and sink lanes. -/ +def netCharge (e : ZeroLayerEvent) : Int := + e.observableCharge + e.underverseCharge + e.sinkCharge + +/-- The neutral closure predicate. -/ +def closesNeutral (e : ZeroLayerEvent) : Bool := + netCharge e == 0 && e.replayReceiptPresent + +/-- Genus-3 zero-charge assumption is explicit: genus=3, chart=genus3, net=0, +and the replay receipt is present. -/ +def genus3ZeroChargeEvent (e : ZeroLayerEvent) : Bool := + e.chart == .genus3 && e.genus == 3 && closesNeutral e + +/-- Decision gate for neutral closure. -/ +def decideZeroLayer (e : ZeroLayerEvent) : ZeroDecision := + if closesNeutral e then .admit + else if netCharge e == 0 then .hold + else .reject + +/-- Canonical fixture: visible +1, Underverse -1, no sink, genus-3 chart. -/ +def genus3BalancedFixture : ZeroLayerEvent := + { chart := .genus3 + , genus := 3 + , observableCharge := 1 + , underverseCharge := -1 + , sinkCharge := 0 + , replayReceiptPresent := true + } + +/-- Same charges, but no replay receipt: balance is only HOLD. -/ +def missingReplayFixture : ZeroLayerEvent := + { genus3BalancedFixture with replayReceiptPresent := false } + +/-- Nonzero net charge rejects the zero-layer claim. -/ +def nonzeroChargeFixture : ZeroLayerEvent := + { genus3BalancedFixture with underverseCharge := 0 } + +theorem genus3BalancedFixture_closes : + genus3ZeroChargeEvent genus3BalancedFixture = true := by + rfl + +theorem missingReplayFixture_holds : + decideZeroLayer missingReplayFixture = .hold := by + rfl + +theorem nonzeroChargeFixture_rejects : + decideZeroLayer nonzeroChargeFixture = .reject := by + rfl + +#eval genus3ZeroChargeEvent genus3BalancedFixture +#eval decideZeroLayer missingReplayFixture +#eval decideZeroLayer nonzeroChargeFixture + +end Semantics.UnderverseZeroLayer diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Kernel/EigenGate.lean b/0-Core-Formalism/lean/Semantics/Semantics/Kernel/EigenGate.lean new file mode 100644 index 00000000..f8184e5b --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Kernel/EigenGate.lean @@ -0,0 +1,180 @@ +/- +EigenGate.lean — The canonical eigengate type. + +Every physical law, every compression check, every routing decision is an +eigenstate condition: ∥G·s − s∥ ≤ τ, where G is the operator defining the +expected invariant, and the residual is the fraction of deviation from identity. + +Residuals live in Q0_16 — the dimensionless pure-fraction type from +FixedPoint.lean. Products stay in [0,1): the multiplicative gate chain +never overflows, and any zero-score gate collapses the entire product. + + verdict : admit if residual=0, hold if ≤ threshold, reject if > + score : 1/(1+r) — proximity to λ=1 eigenspace + route : eigenstate / nearEigenstate / boundary / underverse / error + +Specific physics emerges from WHICH operator G and WHICH calibration constants +parameterize it. The full physical universe is the intersection of λ=1 +eigenspaces for all required gate operators simultaneously. +-/ + +import Semantics.FixedPoint + +namespace Semantics.Kernel + +open Semantics.FixedPoint (Q0_16) + +inductive EigenVerdict where + | admit | hold | reject + deriving Repr, BEq, DecidableEq, Inhabited + +inductive Route where + | eigenstate + | nearEigenstate + | boundary + | underverse + | error + deriving Repr, BEq, DecidableEq, Inhabited + +structure Eigengate (α : Type) where + operator : α → α + residual : α → Q0_16 + threshold : Q0_16 + +def verdict {α : Type} (g : Eigengate α) (s : α) : EigenVerdict := + let r := g.residual s + if r.val == 0 then EigenVerdict.admit + else if r.val ≤ g.threshold.val then EigenVerdict.hold + else EigenVerdict.reject + +def score (r : Q0_16) : Q0_16 := + let denom := Q0_16.add Q0_16.one r + Q0_16.div Q0_16.one denom + +def route {α : Type} (g : Eigengate α) (s : α) (hasReceipt : Bool) : Route := + let v := verdict g s + let r := g.residual s + match v with + | EigenVerdict.admit => + if r.val == 0 then Route.eigenstate + else Route.nearEigenstate + | EigenVerdict.hold => Route.boundary + | EigenVerdict.reject => + if hasReceipt then Route.underverse + else Route.error + +def chainVerdict {α : Type} (gates : List (Eigengate α × Bool)) (s : α) : EigenVerdict := + let required := gates.filter (fun (_, req) => req) |>.map (fun (g, _) => g) + if required.any fun g => verdict g s == EigenVerdict.reject then + EigenVerdict.reject + else if required.any fun g => verdict g s == EigenVerdict.hold then + EigenVerdict.hold + else + EigenVerdict.admit + +def q0Ratio (num den : Nat) : Q0_16 := + if den = 0 then Q0_16.one + else ⟨(Nat.min 32767 ((num * 32767) / den)).toUInt16⟩ + +def shore : Q0_16 := Q0_16.zero + +def approach (N : Nat) : Q0_16 := + if N == 0 then Q0_16.zero + else if N ≥ 16 then Q0_16.one + else + let step := (1 <<< N) - 1 + let maxV := (1 <<< N) + q0Ratio step maxV + +def testGateAllAdmit : Eigengate Q0_16 := + { operator := λ s => s + , residual := λ _ => Q0_16.zero + , threshold := Q0_16.one } + +def testGateAllReject : Eigengate Q0_16 := + { operator := λ s => s + , residual := λ _ => Q0_16.one + , threshold := q0Ratio 1 4 } + +def testGateResidualAtHalf : Eigengate Q0_16 := + { operator := λ s => s + , residual := λ s => if s.val == 0 then Q0_16.zero else Q0_16.half + , threshold := q0Ratio 1 4 } + +def chainFixtureAllAdmit : List (Eigengate Q0_16 × Bool) := + [ (testGateAllAdmit, true), (testGateAllAdmit, true) ] + +def chainFixtureOneRejects : List (Eigengate Q0_16 × Bool) := + [ (testGateAllAdmit, true), (testGateAllReject, true) ] + +def chainFixtureOptionalReject : List (Eigengate Q0_16 × Bool) := + [ (testGateAllAdmit, true), (testGateAllReject, false) ] + +theorem shore_is_zero : shore.val == 0 := rfl + +theorem admit_verdict_on_zero_residual : + verdict testGateAllAdmit Q0_16.zero = EigenVerdict.admit := by + native_decide + +theorem reject_verdict_on_high_residual : + verdict testGateAllReject Q0_16.zero = EigenVerdict.reject := by + native_decide + +theorem score_val_on_zero_residual : + (score Q0_16.zero).val = 32768 := by + native_decide + +theorem chain_all_admit_admits : + chainVerdict chainFixtureAllAdmit Q0_16.zero = EigenVerdict.admit := by + native_decide + +theorem chain_one_rejects_rejects : + chainVerdict chainFixtureOneRejects Q0_16.zero = EigenVerdict.reject := by + native_decide + +theorem chain_optional_reject_no_effect : + chainVerdict chainFixtureOptionalReject Q0_16.zero = EigenVerdict.admit := by + native_decide + +theorem route_admit_zero_residual_is_eigenstate : + route testGateAllAdmit Q0_16.zero true = Route.eigenstate := by + native_decide + +theorem route_reject_no_receipt_is_error : + route testGateAllReject Q0_16.zero false = Route.error := by + native_decide + +theorem route_reject_with_receipt_is_underverse : + route testGateAllReject Q0_16.zero true = Route.underverse := by + native_decide + +theorem approach_bounded (N : Nat) : Q0_16.le (approach N) Q0_16.one := by + by_cases hN0 : N = 0 + · subst hN0; unfold approach Q0_16.le; native_decide + · by_cases hN16 : N ≥ 16 + · unfold approach; simp [hN0, hN16]; unfold Q0_16.le; native_decide + · have hNle : N ≤ 15 := by omega + interval_cases N <;> unfold approach Q0_16.le <;> native_decide + +#eval verdict testGateAllAdmit Q0_16.zero +#eval verdict testGateAllReject Q0_16.zero +#eval verdict testGateResidualAtHalf Q0_16.half + +#eval score Q0_16.zero +#eval score Q0_16.half + +#eval shore + +#eval approach 2 +#eval approach 5 +#eval approach 16 + +#eval chainVerdict chainFixtureAllAdmit Q0_16.zero +#eval chainVerdict chainFixtureOneRejects Q0_16.zero +#eval chainVerdict chainFixtureOptionalReject Q0_16.zero + +#eval route testGateAllAdmit Q0_16.zero true +#eval route testGateAllReject Q0_16.zero true +#eval route testGateAllReject Q0_16.zero false + +end Semantics.Kernel diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Kernel/GateChain.lean b/0-Core-Formalism/lean/Semantics/Semantics/Kernel/GateChain.lean new file mode 100644 index 00000000..0aedd810 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Kernel/GateChain.lean @@ -0,0 +1,56 @@ +/- +GateChain.lean — Multiplicative eigengate composition. + +Imports EigenGate.lean for the canonical Eigengate, EigenVerdict, and +score/verdict/route/chainVerdict primitives. Adds chain-level composition +and product-score computation. +-/ + +import Semantics.FixedPoint +import Semantics.Kernel.EigenGate + +namespace Semantics.Kernel + +open Semantics.FixedPoint (Q0_16) +open Semantics.Kernel (Eigengate EigenVerdict) + +structure ChainGate (α : Type) where + gate : Eigengate α + required : Bool + +abbrev GateChain (α : Type) : Type := List (ChainGate α) + +def chainGatesToTuples {α : Type} (chain : GateChain α) : List (Eigengate α × Bool) := + chain.map fun cg => (cg.gate, cg.required) + +def chainScore {α : Type} (chain : GateChain α) (s : α) : Q0_16 := + let requiredScores := chain + |>.filter (fun cg => cg.required) + |>.map fun cg => score (cg.gate.residual s) + requiredScores.foldl Q0_16.mul Q0_16.one + +def testChainAllAdmit : GateChain Q0_16 := + [ { gate := testGateAllAdmit, required := true } + , { gate := testGateAllAdmit, required := true } ] + +def testChainOptionalOnly : GateChain Q0_16 := + [ { gate := testGateAllAdmit, required := true } + , { gate := testGateAllReject, required := false } ] + +theorem chainCompositionAllAdmit : + chainVerdict (chainGatesToTuples testChainAllAdmit) Q0_16.zero = EigenVerdict.admit := by + native_decide + +theorem chain_optional_reject_preserves_admit : + chainVerdict (chainGatesToTuples testChainOptionalOnly) Q0_16.zero = EigenVerdict.admit := by + native_decide + +theorem chainScore_all_admit_is_one : + chainScore testChainAllAdmit Q0_16.zero = Q0_16.one := by + native_decide + +#eval chainVerdict (chainGatesToTuples testChainAllAdmit) Q0_16.zero +#eval chainVerdict (chainGatesToTuples testChainOptionalOnly) Q0_16.zero +#eval chainScore testChainAllAdmit Q0_16.zero + +end Semantics.Kernel diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Testing/ErdosSurface.lean b/0-Core-Formalism/lean/Semantics/Semantics/Testing/ErdosSurface.lean new file mode 100644 index 00000000..7a5be1cc --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Testing/ErdosSurface.lean @@ -0,0 +1,149 @@ +import Semantics.Testing.ErdosHarness + +namespace Semantics.Testing.ErdosSurface + +open Semantics.Testing.ErdosHarness + +/-! +ErdosSurface.lean + +Pure Lean surface plan for the DAG/FAMM split. Lean owns the finite packet +status model and emits a compact receipt for the Rust surface manager. + +The surface lanes are deliberately treated as acceleration and transport +lanes. They do not promote theorem claims. +-/ + +inductive SurfaceLane where + | leanTrust + | shmControl + | vulkanShader + | h264Transport + | h265Transport + | audioDsp + deriving Repr, DecidableEq + +structure LanePlan where + lane : SurfaceLane + role : String + trustBoundary : String + deriving Repr + +structure FammCount where + domain : String + status : String + count : Nat + deriving Repr, DecidableEq + +def laneName : SurfaceLane -> String + | .leanTrust => "lean_trust" + | .shmControl => "shm_control" + | .vulkanShader => "vulkan_shader" + | .h264Transport => "h264_transport" + | .h265Transport => "h265_transport" + | .audioDsp => "audio_dsp" + +def surfacePlan : List LanePlan := + [ { lane := .leanTrust + role := "packet status model and promotion gate" + trustBoundary := "authoritative finite receipt classifier" } + , { lane := .shmControl + role := "RAM resident payload exchange" + trustBoundary := "transport only; hash and length checked by host" } + , { lane := .vulkanShader + role := "numeric reductions over compact packet counts" + trustBoundary := "acceleration only; results rechecked by Lean/CPU" } + , { lane := .h264Transport + role := "dense packet-frame telemetry transport" + trustBoundary := "lossy unless decoded and hash-verified" } + , { lane := .h265Transport + role := "denser packet-frame telemetry transport" + trustBoundary := "lossy unless decoded and hash-verified" } + , { lane := .audioDsp + role := "streaming DSP metrics over packet waveforms" + trustBoundary := "signal lane only; not proof-bearing" } ] + +def currentFammCounts : List FammCount := + [ { domain := "erdos_gyarfas", status := "verified_has_power_two_cycle", count := 5 } + , { domain := "erdos_mollin_walsh", status := "finite_smoke_pass", count := 3 } + , { domain := "erdos_selfridge", status := "finite_smoke_pass", count := 2 } + , { domain := "erdos_selfridge", status := "invalid_packet", count := 2 } ] + +def totalCount (xs : List FammCount) : Nat := + xs.foldl (fun acc x => acc + x.count) 0 + +def allSurfaceClaimsFinite (xs : List FammCount) : Bool := + xs.all (fun x => + x.status == "verified_has_power_two_cycle" || + x.status == "finite_smoke_pass" || + x.status == "invalid_packet" || + x.status == "detector_anomaly") + +theorem current_surface_claims_are_finite : + allSurfaceClaimsFinite currentFammCounts = true := by + native_decide + +theorem current_surface_total_count : + totalCount currentFammCounts = 12 := by + native_decide + +def escapeJson (s : String) : String := + s.foldl + (fun acc c => + if c == '"' then acc ++ "\\\"" + else if c == '\\' then acc ++ "\\\\" + else if c == '\n' then acc ++ "\\n" + else acc.push c) + "" + +def q (s : String) : String := + "\"" ++ escapeJson s ++ "\"" + +def joinWith (sep : String) : List String -> String + | [] => "" + | x :: xs => xs.foldl (fun acc y => acc ++ sep ++ y) x + +def boolJson (b : Bool) : String := + if b then "true" else "false" + +def lanePlanJson (p : LanePlan) : String := + "{" ++ + q "lane" ++ ":" ++ q (laneName p.lane) ++ "," ++ + q "role" ++ ":" ++ q p.role ++ "," ++ + q "trust_boundary" ++ ":" ++ q p.trustBoundary ++ + "}" + +def countJson (c : FammCount) : String := + "{" ++ + q "domain" ++ ":" ++ q c.domain ++ "," ++ + q "status" ++ ":" ++ q c.status ++ "," ++ + q "count" ++ ":" ++ toString c.count ++ + "}" + +def countsArrayJson (xs : List FammCount) : String := + "[" ++ joinWith "," (xs.map countJson) ++ "]" + +def countValuesJson (xs : List FammCount) : String := + "[" ++ joinWith "," (xs.map (fun x => toString x.count)) ++ "]" + +def lanesJson : String := + "[" ++ joinWith "," (surfacePlan.map lanePlanJson) ++ "]" + +def surfaceReceiptJson : String := + "{" ++ + q "schema" ++ ":" ++ q "erdos_surface_v1" ++ "," ++ + q "claim_boundary" ++ ":" ++ q "surface lanes accelerate or transport; Lean owns promotion gates" ++ "," ++ + q "finite_statuses_only" ++ ":" ++ boolJson (allSurfaceClaimsFinite currentFammCounts) ++ "," ++ + q "total_count" ++ ":" ++ toString (totalCount currentFammCounts) ++ "," ++ + q "counts" ++ ":" ++ countsArrayJson currentFammCounts ++ "," ++ + q "count_values" ++ ":" ++ countValuesJson currentFammCounts ++ "," ++ + q "lanes" ++ ":" ++ lanesJson ++ + "}" + +def main : IO Unit := do + IO.println surfaceReceiptJson + +end Semantics.Testing.ErdosSurface + +def main : IO Unit := + Semantics.Testing.ErdosSurface.main