Track HCMMR sources and ignore generated mirrors

This commit is contained in:
Brandon Schneider 2026-05-11 21:53:32 -05:00
parent 101068083d
commit 9213d9755e
25 changed files with 6428 additions and 0 deletions

77
.github/RRC_OPERATING_CONTRACT.md vendored Normal file
View file

@ -0,0 +1,77 @@
# Rainbow Raccoon Compiler Operating Contract
Status: required collaboration surface
Scope: GitHub-facing contributor and agent guidance
Claim boundary: RRC is an admissibility and receipt gate, not a proof that a
mathematical, physical, medical, financial, or compression claim is true.
## Purpose
The Rainbow Raccoon Compiler (RRC) is the repository's required shape gate for
working with Allaun's research stack. It turns a proposed symbolic compression,
projection, rewrite, or manifold-boundary shortcut into an inspectable decision:
```text
ACCEPT
HOLD
QUARANTINE
```
That decision must be backed by payload identity, a type witness, residual
policy, and replay evidence. A persuasive story is not enough.
## Required Rule
Any nontrivial new idea must be able to answer:
```text
What is the source payload?
What shape does it project into?
What type witness admits that shape?
What residual or sidecar is needed for replay?
What receipt proves the projection did not drift?
Is the result ACCEPT, HOLD, or QUARANTINE?
```
If those answers are missing, the work remains HOLD.
## RRC In The Stack
RRC sits between generative ideas and core promotion:
```text
idea / source / corpus / equation
-> canonical payload
-> RRC projection candidate
-> residual and replay check
-> receipt
-> Lean/GCCL/Omindirection promotion surface
```
It is especially required for:
- logogram and glyph-payload compression
- GCCL representative transitions
- Omindirection atom promotion
- manifold boundary candidates
- HexLogogram Atlas grouping
- LadderLUT and continued-fraction shortcuts
- semantic tear detection
- any external database or sidecar-backed compression path
## Decisions
| Decision | Meaning |
|---|---|
| `ACCEPT` | The projection has a receipt and can replay under its declared law. |
| `HOLD` | The projection may be useful, but evidence, replay, residual, or type witness is incomplete. |
| `QUARANTINE` | The projection is destructive, torn, or unsafe to merge into ordinary token space. |
## Contributor Standard
When contributing to this repository, do not promote a compression or semantic
rewrite because it is elegant. Promote only when the RRC-shaped evidence says it
is admissible.
In plain English: if you want to deal with this stack seriously, bring receipts.
RRC is how those receipts get shaped.

12
.github/assets/README.md vendored Normal file
View file

@ -0,0 +1,12 @@
# GitHub Social Assets
The repository social image is intentionally the Rainbow Raccoon Compiler.
```text
rainbow_raccoon_compiler.png -> source art
social-preview.png -> GitHub-friendly 1280x640 crop
```
Keep this image path stable. The RRC artwork is part of the repository's mental
container: it marks the receipt-gated collaboration surface for compression,
projection, and semantic rewrite work.

20
.gitignore vendored
View file

@ -98,6 +98,26 @@ tools/servo-fetch/
5-Applications/tools-scripts/external/quantum/
5-Applications/tools-scripts/external/typst-cli/
# Local/generated mirrors that should not be ordinary staging surfaces.
# Force-add a specific artifact when it is promoted into repository evidence.
extensions/
6-Documentation/typst/
6-Documentation/tiddlywiki-local/wiki/tiddlers/*.tid
6-Documentation/wiki/Obsidian-connector/Connector Gap Fill *.md
# Downloaded third-party research trees and paper caches.
2-Search-Space/AI-Feynman/
2-Search-Space/AI-Newton/
2-Search-Space/Goedel-Prover-V2/
2-Search-Space/PINNs/
2-Search-Space/alphageometry/
2-Search-Space/neural-conservation-law/
6-Documentation/papers/Downloads_from_internet/
6-Documentation/papers/downloads/
6-Documentation/papers/facebook_pdfs/
6-Documentation/papers/literature/
6-Documentation/papers/supporting-materials/
# Kernel module build artifacts
*.ko
*.mod

13
.vscode/extensions.json vendored Normal file
View file

@ -0,0 +1,13 @@
{
// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
// List of extensions which should be recommended for users of this workspace.
"recommendations": [
],
// List of extensions recommended by Windsurf that should not be recommended for users of this workspace.
"unwantedRecommendations": [
]
}

View file

@ -0,0 +1,90 @@
import Semantics.HCMMR.Core
import Semantics.FixedPoint
import Semantics.Bind
import Semantics.ReceiptCore
import Semantics.Core.FoldedPointManifold
namespace Semantics.HCMMR.Bridge
open Semantics
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16 Q0_16)
open Semantics.FoldedPointManifold (FoldDecision GateOutcome ResolutionDelta TotalInteraction)
open Semantics.ReceiptCore (Receipt ReceiptKind)
-- ═══════════════════════════════════════════════════════════════════
-- §1 FoldDecision ↔ HCMMR GateVerdict
-- ═══════════════════════════════════════════════════════════════════
def gateVerdictFromFoldDecision : FoldDecision → GateVerdict
| FoldDecision.admit => GateVerdict.admit
| FoldDecision.hold => GateVerdict.hold
| FoldDecision.reject => GateVerdict.reject
def foldDecisionFromGateVerdict : GateVerdict → FoldDecision
| GateVerdict.admit => FoldDecision.admit
| GateVerdict.hold => FoldDecision.hold
| GateVerdict.reject => FoldDecision.reject
#eval gateVerdictFromFoldDecision FoldDecision.admit
#eval gateVerdictFromFoldDecision FoldDecision.hold
#eval gateVerdictFromFoldDecision FoldDecision.reject
#eval foldDecisionFromGateVerdict GateVerdict.admit
#eval foldDecisionFromGateVerdict GateVerdict.hold
#eval foldDecisionFromGateVerdict GateVerdict.reject
-- ═══════════════════════════════════════════════════════════════════
-- §2 GateOutcome list → HCMMR GateChain
-- ═══════════════════════════════════════════════════════════════════
def gateChainFromGateOutcomeList (outcomes : List GateOutcome) (names : List String) : GateChain :=
let extra := List.replicate (max 0 (outcomes.length - names.length)) "unnamed"
let padded := names ++ extra
let pairs := List.zip outcomes padded
let gates := pairs.map fun (o, nm) =>
let verdict : GateVerdict := match o with
| GateOutcome.admit => GateVerdict.admit
| GateOutcome.hold => GateVerdict.hold
| GateOutcome.reject => GateVerdict.reject
{ name := nm, required := true, score := Q16_16.one, verdict := verdict }
{ gates := gates }
#eval gateChainFromGateOutcomeList [GateOutcome.admit, GateOutcome.hold, GateOutcome.reject] ["phi", "khi", "psi"]
-- ═══════════════════════════════════════════════════════════════════
-- §3 Bind.Metric → HCMMR Gate
-- ═══════════════════════════════════════════════════════════════════
def bindMetricToGate (m : Metric) : Gate :=
let score := if m.cost.val == 0 then Q16_16.one
else Q16_16.div Q16_16.one m.cost
{ name := m.tensor
, required := true
, score := score
, verdict := if m.cost.val == Q16_16.zero.val then GateVerdict.admit
else if score.val > 0 then GateVerdict.hold
else GateVerdict.reject
}
#eval bindMetricToGate Metric.euclidean
#eval bindMetricToGate { cost := Q16_16.ofInt 2, tensor := "riemannian", torsion := Q16_16.ofInt 1,
reference := "test", history_len := 1 }
-- ═══════════════════════════════════════════════════════════════════
-- §4 Theorems
-- ═══════════════════════════════════════════════════════════════════
theorem foldDecision_roundtrip (v : GateVerdict) :
gateVerdictFromFoldDecision (foldDecisionFromGateVerdict v) = v := by
cases v <;> rfl
theorem foldDecision_roundtrip_admit :
foldDecisionFromGateVerdict (gateVerdictFromFoldDecision FoldDecision.admit) = FoldDecision.admit := by rfl
theorem foldDecision_roundtrip_reject :
foldDecisionFromGateVerdict (gateVerdictFromFoldDecision FoldDecision.reject) = FoldDecision.reject := by rfl
theorem foldDecision_roundtrip_hold :
foldDecisionFromGateVerdict (gateVerdictFromFoldDecision FoldDecision.hold) = FoldDecision.hold := by rfl
end Semantics.HCMMR.Bridge

View file

@ -0,0 +1,362 @@
/-
HCMMR Core.lean — Hyper-CMMR Operadic Meta-Calculus v0.1 typeclass definitions.
This is the typeclass and core structure file. Every other HCMMR module
depends on these definitions. The HCMMR is a typed-gate diagnostic system:
objects enter a 16D transform stack, get decomposed through multiplicative
gates, and produce signed eigenmass with residual receipts. A failed gate
does NOT erase the object — it collapses the validity claim and routes the
residual to the Underverse.
-/
import Semantics.FixedPoint
import Semantics.Bind
import Semantics.ReceiptCore
namespace Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Gate Verdict (admit / hold / reject)
-- ═══════════════════════════════════════════════════════════════════
/--
The three possible outcomes of a gate evaluation, isomorphic to
`FoldedPointManifold.FoldDecision`. A failed gate routes the object's
residual to an alternate path rather than destroying it.
-/
inductive GateVerdict where
| admit
| hold
| reject
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §2 HCMMRObject — the fundamental entity entering the transform stack
-- ═══════════════════════════════════════════════════════════════════
/--
The fundamental entity that enters the HCMMR 16D transform stack.
Carries its symbolic identity, native dimensional home, the metric gate
it targets, origin description, admissibility flag, and receipt chain root.
-/
structure HCMMRObject where
payload : String
nativeDim : Nat
requestedGate : String
source : String
admissible : Bool
receiptRoot : String
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §3 Gate — a single admission gate
-- ═══════════════════════════════════════════════════════════════════
/--
A single gate in the multiplicative admission chain.
`required` gates block the chain on hold or reject.
`score` is in [0, 1] via Q16_16 (0 = total failure, 1 = perfect pass).
-/
structure Gate where
name : String
required : Bool
score : Q16_16
verdict : GateVerdict
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §4 GateChain — ordered list of gates forming a multiplicative series
-- ═══════════════════════════════════════════════════════════════════
/--
An ordered list of gates forming the multiplicative admission series.
The chain passes only if ALL required gates admit.
-/
structure GateChain where
gates : List Gate
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §5 gateChainVerdict — evaluate a GateChain
-- ═══════════════════════════════════════════════════════════════════
/--
Evaluates a GateChain using multiplicative logic:
- If ANY required gate rejects → reject
- If ANY required gate is hold (and none reject) → hold
- If ALL required gates admit → admit
Non-required gates are ignored for chain verdict.
-/
def gateChainVerdict (chain : GateChain) : GateVerdict :=
let requiredGates := chain.gates.filter (fun g => g.required)
if requiredGates.any (fun g => g.verdict == GateVerdict.reject) then
GateVerdict.reject
else if requiredGates.any (fun g => g.verdict == GateVerdict.hold) then
GateVerdict.hold
else
GateVerdict.admit
-- ═══════════════════════════════════════════════════════════════════
-- §6 EigenmassOperator — extracts stable modes
-- ═══════════════════════════════════════════════════════════════════
/--
The eigenmass operator extracts stable structural modes and per-gate
admission scores. Each score field records the corresponding gate's
Q16_16 value in [0, 1]. The canonical multiplicative eigenmass is
computed from these scores via `eigenmassProduct`.
-/
structure EigenmassOperator where
eigenvalue : Q16_16
magnitude : Q16_16
admissibilityScore : Q16_16
invarianceScore : Q16_16
chiralityScore : Q16_16
receiptScore : Q16_16
calibrationScore : Q16_16
projectionScore : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §7 eigenmassProduct — the canonical multiplicative eigenmass M⁺
-- ═══════════════════════════════════════════════════════════════════
/--
Computes the canonical multiplicative eigenmass M⁺:
M⁺ = (λ₁ × A × I × χ × R × Ω_K × Π) / (1 + ε)
If any gate score is zero, the product is zero (multiplicative collapse).
`epsilon` is the residual friction from gate mismatches, passed in as a
Q16_16 value. The denominator is always at least 1.0.
-/
def eigenmassProduct (op : EigenmassOperator) (epsilon : Q16_16) : Q16_16 :=
let gates := #[op.eigenvalue, op.admissibilityScore, op.invarianceScore,
op.chiralityScore, op.receiptScore, op.calibrationScore,
op.projectionScore]
let anyZero := gates.any (fun s => s.val == 0)
if anyZero then
Q16_16.zero
else
let product := gates.foldl Q16_16.mul (Q16_16.ofInt 1)
let denom := Q16_16.add (Q16_16.ofInt 1) epsilon
if denom.val == 0 then
Q16_16.zero
else
Q16_16.div product denom
-- ═══════════════════════════════════════════════════════════════════
-- §8 eigenmassSigned — the signed eigenmass M±
-- ═══════════════════════════════════════════════════════════════════
/--
Computes the signed eigenmass M±:
M±(X) = M⁺(X) M⁻(X)
M⁺ uses the positive-ladder residual ε⁺.
M⁻ uses the same gate scores but with the Underverse-side residual ε⁻
(higher friction yields smaller denominator and more mass penalty).
If the Underverse mass is zero, the signed mass equals the positive mass.
-/
def eigenmassSigned (op : EigenmassOperator) (epsilonPlus epsilonMinus : Q16_16) : Q16_16 :=
let mPlus := eigenmassProduct op epsilonPlus
let mMinus := eigenmassProduct op epsilonMinus
Q16_16.sub mPlus mMinus
-- ═══════════════════════════════════════════════════════════════════
-- §9 Residual — dimensional mismatch friction
-- ═══════════════════════════════════════════════════════════════════
/--
A typed residual scar produced when an object mismatches a gate's
dimensional metric. Each residual carries its domain, Q16_16 magnitude,
and the source gate that produced it.
-/
structure Residual where
domain : String
value : Q16_16
source : String
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §10 DiagnosticReceipt — what a failed gate emits
-- ═══════════════════════════════════════════════════════════════════
/--
Emitted when a gate rejects an object. Records the failed object's
identity, which gate rejected it, the residual scar, an alternate route
for rerouting the residual, and a timestamp.
-/
structure DiagnosticReceipt where
object : String
failedGate : String
residual : Residual
alternateRoute : String
timestamp : Nat
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §11 Fixtures
-- ═══════════════════════════════════════════════════════════════════
/--
A fully passing HCMMRObject with all gates admitting.
Represents an object that survives the full multiplicative chain.
-/
def canonicalFixture : HCMMRObject :=
{ payload := "pythagorean_triple"
, nativeDim := 2
, requestedGate := "L2"
, source := "Euclidean_geometry"
, admissible := true
, receiptRoot := "deadbeef00000000000000000000000000000000000000000000000000000000"
}
/--
An EigenmassOperator for a perfectly passing object: all gate scores
are 1.0 and the eigenvalue is 1.0.
-/
def fullyAdmittingOperator : EigenmassOperator :=
{ eigenvalue := Q16_16.one
, magnitude := Q16_16.one
, admissibilityScore := Q16_16.one
, invarianceScore := Q16_16.one
, chiralityScore := Q16_16.one
, receiptScore := Q16_16.one
, calibrationScore := Q16_16.one
, projectionScore := Q16_16.one
}
/--
An operator where the receipt gate has failed (score = 0).
-/
def receiptFailureOperator : EigenmassOperator :=
{ fullyAdmittingOperator with receiptScore := Q16_16.zero }
/--
A fully admitting chain with all seven canonical gates.
-/
def fullyAdmittingChain : GateChain :=
{ gates :=
[ { name := "Admissibility", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
, { name := "Invariance", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
, { name := "Chirality", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
, { name := "Receipt", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
, { name := "Calibration", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
, { name := "Projection", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
]
}
/--
A chain where the Chirality gate holds.
-/
def chiralityHoldChain : GateChain :=
{ fullyAdmittingChain with
gates := fullyAdmittingChain.gates.map (fun g =>
if g.name == "Chirality" then
{ g with verdict := GateVerdict.hold }
else
g)
}
/--
A chain where the Receipt gate rejects.
-/
def receiptRejectChain : GateChain :=
{ fullyAdmittingChain with
gates := fullyAdmittingChain.gates.map (fun g =>
if g.name == "Receipt" then
{ g with verdict := GateVerdict.reject }
else
g)
}
/--
A chain where an optional/non-required gate rejects — should not affect
the chain verdict.
-/
def optionalRejectChain : GateChain :=
{ fullyAdmittingChain with
gates := fullyAdmittingChain.gates.map (fun g =>
if g.name == "Projection" then
{ g with required := false, verdict := GateVerdict.reject }
else
g)
}
-- ═══════════════════════════════════════════════════════════════════
-- §12 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
When all required gates admit, the chain admits.
-/
theorem gate_chain_all_admit :
gateChainVerdict fullyAdmittingChain = GateVerdict.admit := by
native_decide
/--
A single required reject causes the chain to reject.
-/
theorem gate_chain_one_rejects :
gateChainVerdict receiptRejectChain = GateVerdict.reject := by
native_decide
/--
If a single required gate is hold (and none reject), the chain is hold.
-/
theorem gate_chain_one_holds :
gateChainVerdict chiralityHoldChain = GateVerdict.hold := by
native_decide
/--
An optional gate rejecting does not affect the chain verdict.
-/
theorem gate_chain_optional_reject_ignored :
gateChainVerdict optionalRejectChain = GateVerdict.admit := by
native_decide
/--
If any gate score is zero, eigenmassProduct is zero.
-/
theorem eigenmass_zero_on_any_gate_failure :
eigenmassProduct receiptFailureOperator Q16_16.zero = Q16_16.zero := by
native_decide
/--
When both epsilons are equal, M± = 0 (perfect symmetry in ladder vs underverse).
-/
theorem eigenmass_signed_identity :
eigenmassSigned fullyAdmittingOperator Q16_16.zero Q16_16.zero
= Q16_16.zero := by
native_decide
/--
With nonzero epsilon, the fully admitting operator yields M⁺ < 1.0
(because denominator exceeds 1.0).
-/
theorem eigenmass_product_residual_dampens :
Q16_16.lt (eigenmassProduct fullyAdmittingOperator (Q16_16.ofInt 2)) (Q16_16.ofInt 1) = true := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §13 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
#eval canonicalFixture
#eval gateChainVerdict fullyAdmittingChain
#eval gateChainVerdict chiralityHoldChain
#eval gateChainVerdict receiptRejectChain
#eval gateChainVerdict optionalRejectChain
#eval eigenmassProduct fullyAdmittingOperator Q16_16.zero
#eval eigenmassProduct fullyAdmittingOperator (Q16_16.ofInt 2)
#eval eigenmassProduct receiptFailureOperator Q16_16.zero
#eval eigenmassSigned fullyAdmittingOperator Q16_16.zero Q16_16.zero
#eval eigenmassSigned fullyAdmittingOperator (Q16_16.ofInt 2) (Q16_16.ofInt 4)
end Semantics.HCMMR.Core

View file

@ -0,0 +1,459 @@
/-
BoundaryEigenFire.lean — B_∂ Modal Burn Surface Kernel
Defines the boundary eigenfire field B_∂(x) — the surface projection of the
λ_YAH hyper-eigenspectrum — and the tripartite BoundaryVerdict:
admitted — ‖B_∂‖ ≤ Θ_activation, boundary resolves in current chart
underverseEntry — receipts fail to close, object routes to Underverse shadow
geodesicPromotion — ‖B_∂‖ → ∞, irreconcilable receipts, geodesic opens in ^(n+1)
Core doctrine (per BoundaryEigenFire.md):
A boundary is not a separator line. It is a modal burn surface — the local
superposition surface where encoded state values pile up and interfere.
The "wall of fire" condition is ‖B_∂(x)‖ > Θ_activation: the dominant modal
stack ignites. Which mode dominates determines what the boundary manifests as.
Wormhole throat prediction:
When two objects carry irreconcilable receipts (A_motion→1 meets
ε_displacement=0), B_∂ cannot resolve in ^n. The predicted resolution:
a higher-dimensional geodesic opens (GeodesicPromotion verdict).
Within the 16D stack: dim < 16 → n+1; dim = 16 → loopback compaction (Π gate).
The throat is latent in S3CProjectedGeodesicResolution's resolutionDelta
arithmetic — this is the case where that budget overflows.
Architecture (per DeepSeek review 2026-05-11):
- Imports HyperEigenSpectrum (no reverse dependency)
- GeodesicPromotion is a first-class verdict, not a field
- GeodesicPromotionReceipt references FoldedPointManifold's permeability model
- PromotionType: dimensionalExtrusion (dim<16) | loopbackCompaction (dim=16)
Conventions:
PascalCase types, camelCase functions.
Q16_16 for all numeric fields.
Fin 17 for dimensional slots (0..16).
Namespace: Semantics.HCMMR.Kernels.BoundaryEigenFire
-/
import Semantics.HCMMR.Core
import Semantics.HCMMR.Kernels.HyperEigenSpectrum
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.BoundaryEigenFire
open Semantics.HCMMR.Core
open Semantics.HCMMR.Kernels.HyperEigenSpectrum
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Modal weight vector — the B_∂ projection coefficients
-- ═══════════════════════════════════════════════════════════════════
/--
The α-coefficient vector for the boundary field projection.
B_∂(x) = α_ρ·ρ + α_g·∇ρ + α_T·T + α_σ·σ + α_κ·κ + α_β·β + α_η·η + α_ε·ε
Each α is a Q16_16 weight ∈ [0, 65536]. The vector is obtained by
projecting the HyperEigenSpectrum onto the boundary surface ∂Ω. In this
discrete model, projection = extract the mode scores that are geometrically
"surface-active" rather than interior-active.
Mapping from EigenMode to boundary coefficient:
voidHierarchy → α_ρ (density concentration at boundary)
scarRoughness → α_g (density gradient — scar is a gradient surface)
densitySpectrum→ α_ρ (additional density weight)
lacunarity → α_κ (gap texture ↔ curvature)
topoComponents → α_β (connected components receipt)
topoTunnels → α_β (tunnel receipt)
topoVoids → α_β (void receipt)
percolation → α_g (connectivity gradient)
curvature → α_κ (direct curvature)
coupling → α_η (medium coupling at boundary)
residual → α_ε (unexplained boundary term)
-/
structure ModalWeights where
alphaDensity : Q16_16 -- α_ρ density / void
alphaGradient : Q16_16 -- α_g density gradient / scar / percolation
alphaThermal : Q16_16 -- α_T thermal state
alphaStress : Q16_16 -- α_σ mechanical stress / strain
alphaCurvature : Q16_16 -- α_κ curvature / lacunarity
alphaTopology : Q16_16 -- α_β topology receipt (β₀+β₁+β₂ combined)
alphaCoupling : Q16_16 -- α_η medium coupling
alphaResidual : Q16_16 -- α_ε unexplained residual
deriving Repr, BEq, DecidableEq, Inhabited
/--
Project a HyperEigenSpectrum onto the boundary ModalWeights.
The projection maps each EigenMode component onto its primary boundary
coefficient using the mapping described in `ModalWeights`.
-/
def projectToBoundary (s : HyperEigenSpectrum) : ModalWeights :=
let b := s.bind
-- density: void + density spectrum averaged
let ρ : Q16_16 := ⟨(b.omegaM.val / 2 + b.dQ.val / 2)⟩
-- gradient: scar roughness + percolation averaged
let g : Q16_16 := ⟨(b.rK.val / 2 + b.perc.val / 2)⟩
-- thermal: not directly in BindOperator — proxy via coupling
let T : Q16_16 := ⟨b.eta.val / 2⟩
-- stress: proxy via coupling + scar
let σ : Q16_16 := ⟨(b.eta.val / 2 + b.rK.val / 4)⟩
-- curvature: direct + lacunarity
let κ : Q16_16 := ⟨(b.curv.val / 2 + b.lacun.val / 2)⟩
-- topology: β₀ + β₁ + β₂ averaged
let β : Q16_16 := ⟨(b.bk0.val / 3 + b.bk1.val / 3 + b.bk2.val / 3)⟩
-- coupling: direct
let η : Q16_16 := b.eta
-- residual: direct
let ε : Q16_16 := b.eps
{ alphaDensity := ρ
, alphaGradient := g
, alphaThermal := T
, alphaStress := σ
, alphaCurvature := κ
, alphaTopology := β
, alphaCoupling := η
, alphaResidual := ε }
/--
Compute the L∞ norm of the ModalWeights — the dominant boundary mode strength.
‖B_∂‖ = max(α_i).
-/
def modalNorm (w : ModalWeights) : Q16_16 :=
let vals := #[w.alphaDensity, w.alphaGradient, w.alphaThermal, w.alphaStress,
w.alphaCurvature, w.alphaTopology, w.alphaCoupling, w.alphaResidual]
vals.foldl (fun acc v => if v.val > acc.val then v else acc) ⟨0⟩
-- ═══════════════════════════════════════════════════════════════════
-- §2 BoundaryField — the full projected boundary surface state
-- ═══════════════════════════════════════════════════════════════════
/--
The boundary field B_∂(x) for one object at one boundary point.
`spectrum` is the λ_YAH eigenspectrum of the object's interior.
`weights` is the projected ModalWeights onto ∂Ω.
`activationNorm` is ‖B_∂(x)‖ = max(α_i).
`sourceDim` is the current dimensional chart (Fin 17, enforcing ≤ 16 cap).
`receiptsClosed` tracks whether the receipt chain closes at this boundary.
-/
structure BoundaryField where
spectrum : HyperEigenSpectrum
weights : ModalWeights
activationNorm : Q16_16
sourceDim : Fin 17
receiptsClosed : Bool
deriving Repr, Inhabited
/--
Construct a BoundaryField from a HyperEigenSpectrum and dimensional chart.
-/
def BoundaryField.fromSpectrum (s : HyperEigenSpectrum) (dim : Fin 17)
(receiptsClosed : Bool := true) : BoundaryField :=
let w := projectToBoundary s
{ spectrum := s
, weights := w
, activationNorm := modalNorm w
, sourceDim := dim
, receiptsClosed }
-- ═══════════════════════════════════════════════════════════════════
-- §3 Activation threshold and EigenFire condition
-- ═══════════════════════════════════════════════════════════════════
/--
EigenFire activation threshold Θ_activation.
A boundary "ignites" when its dominant modal weight exceeds this value.
Set at 75% of Q16_16 range: 0.75 × 65536 = 49152.
Below threshold: boundary is passive (transmissive, cool).
Above threshold: boundary manifests actively (thermal, mechanical, topological).
At max (65536): boundary is at saturation — potential geodesic puncture.
-/
def activationThreshold : Q16_16 := ⟨49152⟩
/--
Puncture threshold — ‖B_∂‖ at which the boundary can no longer resolve in
the current chart and geodesic promotion is triggered.
Set at 95% of Q16_16 range: 0.95 × 65536 = 62259.
-/
def punctureThreshold : Q16_16 := ⟨62259⟩
/--
EigenFire condition: activationNorm > Θ_activation.
-/
def isEigenFire (f : BoundaryField) : Bool :=
f.activationNorm.val > activationThreshold.val
/--
Puncture condition: activationNorm > Θ_puncture AND receipts failed to close.
Both conditions required: high activation alone may be a hot-but-admissible boundary.
Receipts failing to close indicates irreconcilable states.
-/
def isPuncture (f : BoundaryField) : Bool :=
f.activationNorm.val > punctureThreshold.val && !f.receiptsClosed
-- ═══════════════════════════════════════════════════════════════════
-- §4 Dominant manifestation — what the boundary looks like
-- ═══════════════════════════════════════════════════════════════════
/--
The dominant manifestation class of an active boundary.
What appears when B_∂ ignites depends on which modal coefficient dominates.
-/
inductive BoundaryManifestation
| thermal -- α_T dominant: glow, flame, plasma sheath
| mechanical -- α_σ dominant: fracture band, impact crater
| compression -- α_g dominant: shockwave, sonic boom
| coupling -- α_η dominant: ionization, EM emission, energy deposition
| geometric -- α_κ dominant: caustic, Riemannian tear, curvature singularity
| topological -- α_β dominant: topology tear, handle attachment, homology jump
| density -- α_ρ dominant: density spike, void wall
| residual -- α_ε dominant: Underverse scar, unexplained anomaly
deriving Repr, BEq, DecidableEq, Inhabited
/--
Identify the dominant manifestation from ModalWeights.
-/
def dominantManifestation (w : ModalWeights) : BoundaryManifestation :=
let candidates : Array (BoundaryManifestation × Q16_16) :=
#[(.thermal, w.alphaThermal)
, (.mechanical, w.alphaStress)
, (.compression,w.alphaGradient)
, (.coupling, w.alphaCoupling)
, (.geometric, w.alphaCurvature)
, (.topological,w.alphaTopology)
, (.density, w.alphaDensity)
, (.residual, w.alphaResidual)]
let best := candidates.foldl
(fun acc c => if c.2.val > acc.2.val then c else acc)
(.residual, ⟨0⟩)
best.1
-- ═══════════════════════════════════════════════════════════════════
-- §5 BoundaryVerdict — the tripartite gate outcome
-- ═══════════════════════════════════════════════════════════════════
/--
How the dimensional promotion resolves when ‖B_∂‖ → puncture threshold.
`dimensionalExtrusion`: sourceDim < 16 → geodesic opens in dim+1.
`loopbackCompaction`: sourceDim = 16 → Π gate activates loopback to
compactified chart (stack reset, not stack exit).
-/
inductive PromotionType
| dimensionalExtrusion -- opens dim+1 within 0..16 cap
| loopbackCompaction -- at dim=16, Π loops back to compactified chart
deriving Repr, BEq, DecidableEq, Inhabited
/--
Receipt for a geodesic promotion event.
`sourceChart` : Fin 17 — the dimensional chart where the puncture occurred
`targetChart` : Fin 17 — the promoted chart (sourceChart+1, or 0 for loopback)
`promotionType` : how the promotion resolves
`throatRadius` : Q16_16 — estimated throat opening size (from activation norm)
`spectrumAtPuncture` : the λ_YAH snapshot at the moment of puncture — what
eigenmode distribution caused the throat to open
-/
structure GeodesicPromotionReceipt where
sourceChart : Fin 17
targetChart : Fin 17
promotionType : PromotionType
throatRadius : Q16_16
spectrumAtPuncture : HyperEigenSpectrum
deriving Repr, Inhabited
/--
Compute the GeodesicPromotionReceipt for a boundary that has reached puncture.
-/
def makePromotionReceipt (f : BoundaryField) : GeodesicPromotionReceipt :=
let src := f.sourceDim
-- Compute target chart: extrude to n+1 (capped at 16), or loopback to 0 at dim 16.
let tgtVal : Nat := if src.val < 16 then src.val + 1 else 0
-- tgtVal ≤ 16 < 17 in both branches: if src.val<16 then src.val+1 ≤ 16, else 0 ≤ 16.
let tgt : Fin 17 := ⟨tgtVal % 17, Nat.mod_lt _ (by norm_num)⟩
let ptype : PromotionType :=
if src.val < 16 then .dimensionalExtrusion else .loopbackCompaction
{ sourceChart := src
, targetChart := tgt
, promotionType := ptype
, throatRadius := f.activationNorm
, spectrumAtPuncture := f.spectrum }
/--
The tripartite boundary verdict.
- `admitted (receipt)` : boundary resolves in current chart, receipt emitted
- `underverseEntry (receipt)` : activation within bounds but receipts don't close;
object routes to Underverse shadow with typed receipt
- `geodesicPromotion (receipt)`: boundary saturates, dimensional puncture opens,
full promotion receipt emitted
-/
inductive BoundaryVerdict
| admitted (manifestation : BoundaryManifestation) (isHot : Bool)
| underverseEntry (manifestation : BoundaryManifestation) (norm : Q16_16)
| geodesicPromotion (promo : GeodesicPromotionReceipt)
deriving Repr, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §6 Full EigenFire gate
-- ═══════════════════════════════════════════════════════════════════
/--
Full typed receipt for one boundary evaluation.
-/
structure EigenFireReceipt where
field : BoundaryField
manifestation : BoundaryManifestation
isEigenFire : Bool
isPuncture : Bool
verdict : BoundaryVerdict
deriving Repr, Inhabited
/--
Evaluate the eigenfire gate for a boundary field.
Decision logic (series circuit):
1. isPuncture? → GeodesicPromotion (irreconcilable receipts, throat opens)
2. !receiptsClosed (but below puncture)? → UnderverseEntry
3. isEigenFire (hot boundary, receipts close)? → Admitted hot
4. otherwise → Admitted cool
-/
def eigenFireGate (f : BoundaryField) : EigenFireReceipt :=
let manif := dominantManifestation f.weights
let fire := isEigenFire f
let punct := isPuncture f
let verdict :=
if punct then
BoundaryVerdict.geodesicPromotion (makePromotionReceipt f)
else if !f.receiptsClosed then
BoundaryVerdict.underverseEntry manif f.activationNorm
else
BoundaryVerdict.admitted manif fire
{ field := f
, manifestation := manif
, isEigenFire := fire
, isPuncture := punct
, verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §7 Collision combinator — irreconcilable receipts
-- ═══════════════════════════════════════════════════════════════════
/--
Model the collision of two objects at a shared boundary.
The combined boundary field is formed by taking the component-wise maximum
of each object's projected modal weights — representing the "pile-up" of
both objects' encoded states at the interface.
`receiptsClosed` is false when the two objects have conflicting dominant modes
(e.g., one has maximal coupling, the other has zero coupling — irreconcilable).
-/
def collide (f1 f2 : BoundaryField) : BoundaryField :=
let w1 := f1.weights
let w2 := f2.weights
-- pile-up: take max of each modal weight
let combined : ModalWeights :=
{ alphaDensity := if w1.alphaDensity.val ≥ w2.alphaDensity.val then w1.alphaDensity else w2.alphaDensity
, alphaGradient := if w1.alphaGradient.val ≥ w2.alphaGradient.val then w1.alphaGradient else w2.alphaGradient
, alphaThermal := if w1.alphaThermal.val ≥ w2.alphaThermal.val then w1.alphaThermal else w2.alphaThermal
, alphaStress := if w1.alphaStress.val ≥ w2.alphaStress.val then w1.alphaStress else w2.alphaStress
, alphaCurvature := if w1.alphaCurvature.val ≥ w2.alphaCurvature.val then w1.alphaCurvature else w2.alphaCurvature
, alphaTopology := if w1.alphaTopology.val ≥ w2.alphaTopology.val then w1.alphaTopology else w2.alphaTopology
, alphaCoupling := if w1.alphaCoupling.val ≥ w2.alphaCoupling.val then w1.alphaCoupling else w2.alphaCoupling
, alphaResidual := if w1.alphaResidual.val ≥ w2.alphaResidual.val then w1.alphaResidual else w2.alphaResidual }
-- irreconcilable: dominant modes differ AND both are strong
let dom1 := dominantManifestation w1
let dom2 := dominantManifestation w2
let irreconcilable := dom1 != dom2
&& f1.activationNorm.val > punctureThreshold.val
&& f2.activationNorm.val > punctureThreshold.val
{ spectrum := f1.spectrum -- use first object's interior as reference
, weights := combined
, activationNorm := modalNorm combined
, sourceDim := f1.sourceDim
, receiptsClosed := !irreconcilable }
-- ═══════════════════════════════════════════════════════════════════
-- §8 Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- Cool boundary: low activation, receipts close → Admitted cool.
def coolBoundary : BoundaryField :=
BoundaryField.fromSpectrum
(fromBind
{ omegaM := ⟨9830⟩, rK := ⟨6554⟩, dQ := ⟨3277⟩, lacun := ⟨3277⟩
, bk0 := ⟨1638⟩, bk1 := ⟨1638⟩, bk2 := ⟨1638⟩
, perc := ⟨3277⟩, curv := ⟨6554⟩, eta := ⟨3277⟩, eps := ⟨1638⟩ }
⟨0⟩)
⟨4, by omega⟩
true
#eval (eigenFireGate coolBoundary).verdict
-- expected: BoundaryVerdict.admitted ... false (cool, not eigenfire)
-- Hot wall: coupling and stress peak, receipts still close → Admitted hot.
def hotWallBind : BindOperator :=
{ omegaM := ⟨13107⟩, rK := ⟨52429⟩, dQ := ⟨26214⟩, lacun := ⟨16384⟩
, bk0 := ⟨6554⟩, bk1 := ⟨19661⟩, bk2 := ⟨6554⟩
, perc := ⟨26214⟩, curv := ⟨45875⟩, eta := ⟨58982⟩, eps := ⟨9830⟩ }
def hotWall : BoundaryField :=
BoundaryField.fromSpectrum (fromBind hotWallBind ⟨32768⟩) ⟨8, by omega⟩ true
#eval (eigenFireGate hotWall).verdict
-- expected: BoundaryVerdict.admitted .coupling true (eigenfire, coupling dominant)
-- Underverse: receipts don't close, below puncture.
def underverseBoundary : BoundaryField :=
{ (BoundaryField.fromSpectrum (fromBind hotWallBind ⟨32768⟩) ⟨8, by omega⟩ false)
with receiptsClosed := false }
#eval (eigenFireGate underverseBoundary).verdict
-- expected: BoundaryVerdict.underverseEntry ...
-- Wormhole throat: unstoppable force meets immovable object.
-- Object A: maximal coupling (unstoppable, motion eigenvalue → max)
def unstoppableForce : BoundaryField :=
BoundaryField.fromSpectrum
(fromBind
{ omegaM := ⟨3277⟩, rK := ⟨3277⟩, dQ := ⟨3277⟩, lacun := ⟨3277⟩
, bk0 := ⟨3277⟩, bk1 := ⟨3277⟩, bk2 := ⟨3277⟩
, perc := ⟨3277⟩, curv := ⟨3277⟩, eta := ⟨65535⟩, eps := ⟨1638⟩ }
⟨65535⟩)
⟨8, by omega⟩ true
-- Object B: zero coupling but maximal density, topology, and curvature —
-- immovable because its density/topology modes dominate at maximum.
-- alphaDensity = (omegaM/2 + dQ/2) = (32767 + 32767) = 65534 > puncture threshold.
def immovableObject : BoundaryField :=
BoundaryField.fromSpectrum
(fromBind
{ omegaM := ⟨65535⟩, rK := ⟨65535⟩, dQ := ⟨65535⟩, lacun := ⟨65535⟩
, bk0 := ⟨65535⟩, bk1 := ⟨65535⟩, bk2 := ⟨65535⟩
, perc := ⟨65535⟩, curv := ⟨65535⟩, eta := ⟨0⟩, eps := ⟨1638⟩ }
⟨65535⟩)
⟨8, by omega⟩ true
def throatCollision : BoundaryField := collide unstoppableForce immovableObject
#eval throatCollision.receiptsClosed
-- expected: false (irreconcilable: coupling vs void, both above puncture threshold)
#eval (eigenFireGate throatCollision).verdict
-- expected: BoundaryVerdict.geodesicPromotion { sourceChart := 8, targetChart := 9, ... }
-- Check promotion type at dim 16 → loopback.
def dim16Field : BoundaryField :=
{ throatCollision with sourceDim := ⟨16, by omega⟩ }
#eval match (eigenFireGate dim16Field).verdict with
| .geodesicPromotion r => r.promotionType
| _ => PromotionType.dimensionalExtrusion
-- expected: PromotionType.loopbackCompaction (at dim=16, Π gate loops back)
end Semantics.HCMMR.Kernels.BoundaryEigenFire

View file

@ -0,0 +1,102 @@
/-
FAMMScarMemory.lean — FAMM frustration/scar memory kernel wrapped around field steps.
Φ_FAMM = exp[-γ(Σ² + I_lock + Δφ)], where Σ² = accumulated scar energy,
I_lock = interference penalty, Δφ = phase mismatch. High frustration suppresses
step magnitude; low frustration permits aggressive exploration.
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.FAMMScarMemory
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
structure FAMMScar where
frustrationEnergy : Q16_16
interferenceLock : Q16_16
phaseMismatch : Q16_16
dampingCoefficient : Q16_16
scarHistory : List String
deriving Repr, BEq, DecidableEq, Inhabited
def fammBias (scar : FAMMScar) : Q16_16 :=
let sigma2 := scar.frustrationEnergy
let iLock := scar.interferenceLock
let dPhi := scar.phaseMismatch
let arg := scar.dampingCoefficient * (sigma2 + iLock + dPhi)
Q16_16.expNeg arg
def applyFAMMBias (delta : Q16_16) (scar : FAMMScar) : Q16_16 :=
let bias := fammBias scar
delta * bias
def recordScar (scar : FAMMScar) (event : String) (newResidual : Q16_16) : FAMMScar :=
let energyDelta := Q16_16.sat01 newResidual
{ frustrationEnergy := scar.frustrationEnergy + energyDelta
, interferenceLock := scar.interferenceLock
, phaseMismatch := scar.phaseMismatch + energyDelta
, dampingCoefficient := scar.dampingCoefficient
, scarHistory := event :: scar.scarHistory
}
def resetFrustration (scar : FAMMScar) (decayFactor : Q16_16) : FAMMScar :=
{ frustrationEnergy := scar.frustrationEnergy * decayFactor
, interferenceLock := scar.interferenceLock * decayFactor
, phaseMismatch := scar.phaseMismatch * decayFactor
, dampingCoefficient := scar.dampingCoefficient
, scarHistory := scar.scarHistory
}
def fammMemoryGate : Gate :=
{ name := "FAMMScarMemory"
, required := false
, score := Q16_16.one
, verdict := GateVerdict.admit
}
def fixtureScar : FAMMScar :=
{ frustrationEnergy := Q16_16.one
, interferenceLock := Q16_16.zero
, phaseMismatch := Q16_16.zero
, dampingCoefficient := Q16_16.one
, scarHistory := ["initial"]
}
def fixtureHighScar : FAMMScar :=
{ frustrationEnergy := Q16_16.ofInt 10
, interferenceLock := Q16_16.ofInt 3
, phaseMismatch := Q16_16.one
, dampingCoefficient := Q16_16.two
, scarHistory := ["collision_1", "rejection_2", "phase_error_3"]
}
theorem famm_gate_name_correct : fammMemoryGate.name = "FAMMScarMemory" := by
rfl
theorem famm_gate_verdict_admits : fammMemoryGate.verdict = GateVerdict.admit := by
rfl
theorem fixtureScar_initial_history : fixtureScar.scarHistory.length = 1 := by
native_decide
theorem fixtureHighScar_history_length : fixtureHighScar.scarHistory.length = 3 := by
native_decide
theorem reset_does_not_change_history_length : (resetFrustration fixtureScar (Q16_16.ofRatio 1 2)).scarHistory.length = fixtureScar.scarHistory.length := by
native_decide
theorem record_extends_history : (recordScar fixtureScar "collision_at_3" Q16_16.one).scarHistory.length = fixtureScar.scarHistory.length + 1 := by
native_decide
#eval fammBias fixtureScar
#eval fammBias fixtureHighScar
#eval applyFAMMBias (Q16_16.ofInt 7) fixtureScar
#eval applyFAMMBias (Q16_16.ofInt 7) fixtureHighScar
#eval recordScar fixtureScar "gate_hold" (Q16_16.ofRatio 3 10)
#eval resetFrustration fixtureHighScar (Q16_16.ofRatio 1 4)
#eval fammMemoryGate
end Semantics.HCMMR.Kernels.FAMMScarMemory

View file

@ -0,0 +1,400 @@
/-
HyperEigenSpectrum.lean — λ_YAH Scale-Regime Eigenvalue Kernel
Defines the λ_YAH (You-Are-Here) hyper-eigenspectrum: a scale-dependent
operator whose eigenspectrum encodes the dominant active physics regime of
an object at a given observer scale, combining:
Ω_M — Menger-like void hierarchy
R_K — Koch-like boundary scar roughness
D_q — multifractal density spectrum
Λ — lacunarity / gap texture
β_k — persistent topology receipts (β₀, β₁, β₂)
P — percolation / web connectivity
C — curvature / Minkowski geometry
η — medium-coupling coefficient
ε — unexplained residual
The dominant eigenvalue λ_dom = eigenvalues[dominantIdx] tells you which
physics chart is active. A large or discontinuous Δλ_dom signals a regime
transition.
Architecture (per DeepSeek review 2026-05-11):
- Separate from EigenmassOperator (different mathematics: spectrum vs. product)
- `fromEigenmassOperator` provides backward-compatible constructor path
- `BoundaryEigenFire.lean` imports this; not the reverse
Conventions:
PascalCase types, camelCase functions.
Q16_16 for all numeric fields.
Array Q16_16 for eigenvalue vectors.
Namespace: Semantics.HCMMR.HyperEigenSpectrum
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.HyperEigenSpectrum
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 BindOperator — the nine-component shape-state descriptor
-- ═══════════════════════════════════════════════════════════════════
/--
The nine-component Bind operator that feeds λ_YAH.
Each field is a Q16_16 score in [0, 65536] (= [0, 1.0] normalised):
- 0 = this mode contributes nothing
- 65536 = this mode is fully active / maximally dominant
`bk0`, `bk1`, `bk2` are the three Betti number receipts (connected
components, tunnels, voids); they are stored separately because topology
persistence receipts are structurally different from continuous field scores.
-/
structure BindOperator where
omegaM : Q16_16 -- Ω_M Menger void hierarchy
rK : Q16_16 -- R_K Koch boundary roughness / scar
dQ : Q16_16 -- D_q multifractal density spectrum
lacun : Q16_16 -- Λ lacunarity / gap texture
bk0 : Q16_16 -- β₀ topology: connected components
bk1 : Q16_16 -- β₁ topology: tunnels / loops
bk2 : Q16_16 -- β₂ topology: enclosed voids
perc : Q16_16 -- P percolation / web connectivity
curv : Q16_16 -- C curvature / Minkowski geometry
eta : Q16_16 -- η medium-coupling coefficient
eps : Q16_16 -- ε unexplained residual
deriving Repr, BEq, DecidableEq, Inhabited
/-- Number of components in a BindOperator. -/
def BindOperator.size : Nat := 11
/-- Flatten a BindOperator to an Array of Q16_16 values. -/
def BindOperator.toArray (b : BindOperator) : Array Q16_16 :=
#[b.omegaM, b.rK, b.dQ, b.lacun, b.bk0, b.bk1, b.bk2, b.perc, b.curv, b.eta, b.eps]
/-- Human-readable labels for each BindOperator component, in array order. -/
def BindOperator.labels : Array String :=
#["Ω_M(void)", "R_K(scar)", "D_q(density)", "Λ(lacunarity)",
"β₀(components)", "β₁(tunnels)", "β₂(voids)",
"P(percolation)", "C(curvature)", "η(coupling)", "ε(residual)"]
-- ═══════════════════════════════════════════════════════════════════
-- §2 EigenMode — named index into the BindOperator array
-- ═══════════════════════════════════════════════════════════════════
/--
Named index into the BindOperator component array.
Mirrors `BindOperator.toArray` ordering exactly.
-/
inductive EigenMode
| voidHierarchy -- index 0: Ω_M
| scarRoughness -- index 1: R_K
| densitySpectrum -- index 2: D_q
| lacunarity -- index 3: Λ
| topoComponents -- index 4: β₀
| topoTunnels -- index 5: β₁
| topoVoids -- index 6: β₂
| percolation -- index 7: P
| curvature -- index 8: C
| coupling -- index 9: η
| residual -- index 10: ε
deriving Repr, BEq, DecidableEq, Inhabited
def EigenMode.toIndex : EigenMode → Nat
| .voidHierarchy => 0
| .scarRoughness => 1
| .densitySpectrum => 2
| .lacunarity => 3
| .topoComponents => 4
| .topoTunnels => 5
| .topoVoids => 6
| .percolation => 7
| .curvature => 8
| .coupling => 9
| .residual => 10
def EigenMode.label : EigenMode → String
| .voidHierarchy => "Ω_M: Menger void hierarchy"
| .scarRoughness => "R_K: Koch boundary scar"
| .densitySpectrum => "D_q: multifractal density"
| .lacunarity => "Λ: lacunarity / gap texture"
| .topoComponents => "β₀: connected components"
| .topoTunnels => "β₁: topological tunnels"
| .topoVoids => "β₂: enclosed voids"
| .percolation => "P: percolation connectivity"
| .curvature => "C: curvature / Minkowski"
| .coupling => "η: medium coupling"
| .residual => "ε: unexplained residual"
-- ═══════════════════════════════════════════════════════════════════
-- §3 HyperEigenSpectrum — the λ_YAH eigenvalue structure
-- ═══════════════════════════════════════════════════════════════════
/--
The λ_YAH hyper-eigenspectrum for one object at one observer scale.
`eigenvalues` is an Array of Q16_16 values, one per BindOperator component,
sorted descending — the dominant mode is always at index `dominantIdx = 0`
by convention (or stored explicitly if sorting is too expensive for a gate).
`weights` holds the raw BindOperator component values before normalisation,
preserved for receipt-chain traceability.
`regimeTransition` is set when the dominant eigenvalue has shifted since
the previous scale step (Δλ_dom is large or discontinuous).
`sourceScale` records the observer scale at which this spectrum was
computed (Q16_16, units are model-native: e.g., log₁₀(r/r₀)).
-/
structure HyperEigenSpectrum where
bind : BindOperator
eigenvalues : Array Q16_16 -- sorted descending by value
dominantIdx : Nat -- index into eigenvalues of the dominant mode
regimeTransition : Bool -- Δλ_dom was large at this scale step
sourceScale : Q16_16 -- observer scale r (log-normalised)
deriving Repr, Inhabited
/-- Total number of eigenvalue components. -/
def HyperEigenSpectrum.size (s : HyperEigenSpectrum) : Nat :=
s.eigenvalues.size
/-- Dominant eigenvalue (λ_dom). -/
def HyperEigenSpectrum.lambdaDom (s : HyperEigenSpectrum) : Q16_16 :=
s.eigenvalues.getD s.dominantIdx ⟨0⟩
/-- Return the mode label for the dominant eigenvalue. -/
def HyperEigenSpectrum.dominantLabel (s : HyperEigenSpectrum) : String :=
BindOperator.labels.getD s.dominantIdx "unknown"
-- ═══════════════════════════════════════════════════════════════════
-- §4 Spectrum construction
-- ═══════════════════════════════════════════════════════════════════
/--
Sort an Array Q16_16 descending by value.
Returns the sorted array and the original index of the maximum element
(= the dominant mode index after sorting = 0, but we keep it explicit).
-/
private def sortDescending (arr : Array Q16_16) : Array Q16_16 :=
arr.toList.mergeSort (fun a b => a.val ≥ b.val) |>.toArray
/--
Find the index of the maximum value in an Array Q16_16.
Returns 0 for empty arrays.
-/
private def argmax (arr : Array Q16_16) : Nat :=
let rec go (i : Nat) (bestIdx : Nat) (bestVal : UInt32) : Nat :=
if i ≥ arr.size then bestIdx
else
let v := arr[i]!.val
if v > bestVal then go (i + 1) i v
else go (i + 1) bestIdx bestVal
go 0 0 0
/--
Compute the HyperEigenSpectrum from a BindOperator at a given observer scale.
The eigenvalues are the raw component scores sorted descending.
`regimeTransition` is set if the dominant eigenvalue exceeds the second by
a ratio of more than 2:1 (the dominant mode is clearly separated — indicates
a strong regime, not a mixed state).
`prevDominantVal` is the dominant eigenvalue from the previous scale step;
if provided and the new dominant differs by more than 25% (16384 Q16 units),
`regimeTransition` is set.
-/
def fromBind (b : BindOperator) (scale : Q16_16)
(prevDominantVal : Option Q16_16 := none) : HyperEigenSpectrum :=
let raw := b.toArray
let sorted := sortDescending raw
let domVal := sorted.getD 0 ⟨0⟩
let secondVal := sorted.getD 1 ⟨0⟩
-- Regime transition: dominant shifted >25% from previous, or >2× second mode
let transitionFromPrev :=
match prevDominantVal with
| none => false
| some prev =>
let diff := if domVal.val ≥ prev.val then domVal.val - prev.val else prev.val - domVal.val
diff > 16384 -- 25% of Q16_16 range
let transitionFromGap :=
secondVal.val > 0 && domVal.val > secondVal.val * 2
{ bind := b
, eigenvalues := sorted
, dominantIdx := 0 -- sorted: dominant is always first
, regimeTransition := transitionFromPrev || transitionFromGap
, sourceScale := scale }
/--
Construct a HyperEigenSpectrum from an existing EigenmassOperator.
Seeds the BindOperator using the seven gate scores from EigenmassOperator:
eigenvalue → splits between omegaM and rK (spectral structure)
admissibilityScore → dQ (density/admissibility coupling)
invarianceScore → lacun + bk0 (invariant structure, topology)
chiralityScore → bk1 (chirality ~ topological tunnel orientation)
receiptScore → bk2 + perc (receipt chain ~ void/connectivity)
calibrationScore → curv (constant calibration ~ curvature anchoring)
projectionScore → eta + eps (projection ~ coupling + residual)
This is a lossy lift — 7 scalars seed 11 slots — but provides backward
compatibility for all existing gate chains.
-/
def fromEigenmassOperator (op : EigenmassOperator) (scale : Q16_16 := ⟨0⟩) : HyperEigenSpectrum :=
let half (q : Q16_16) : Q16_16 := ⟨q.val / 2⟩
let b : BindOperator :=
{ omegaM := half op.eigenvalue
, rK := half op.eigenvalue
, dQ := op.admissibilityScore
, lacun := half op.invarianceScore
, bk0 := half op.invarianceScore
, bk1 := op.chiralityScore
, bk2 := half op.receiptScore
, perc := half op.receiptScore
, curv := op.calibrationScore
, eta := half op.projectionScore
, eps := half op.projectionScore }
fromBind b scale
-- ═══════════════════════════════════════════════════════════════════
-- §5 Regime classification
-- ═══════════════════════════════════════════════════════════════════
/--
The physics regime implied by the dominant eigenmode.
Maps from EigenMode to a human-readable physics chart label.
-/
def regimeLabel (mode : EigenMode) : String :=
match mode with
| .voidHierarchy => "Menger/void — cosmic web, interior-void physics"
| .scarRoughness => "Koch/scar — boundary fracture, surface roughness"
| .densitySpectrum => "Multifractal density — turbulence, galaxy clustering"
| .lacunarity => "Lacunarity — gap texture, porosity regime"
| .topoComponents => "Topological β₀ — connectivity, island counting"
| .topoTunnels => "Topological β₁ — tunnel/loop regime"
| .topoVoids => "Topological β₂ — enclosed void regime"
| .percolation => "Percolation — web/filament connectivity"
| .curvature => "Curvature — Riemannian / Minkowski geometry"
| .coupling => "Coupling — energy deposition, EM interaction"
| .residual => "Residual — Underverse scar, unexplained anomaly"
/--
Return the dominant EigenMode for a spectrum.
Since eigenvalues are sorted descending, the dominant mode is the one whose
original BindOperator position had the highest value.
We recover the original position by finding which entry in the sorted array
matches the raw bind value at each EigenMode index.
-/
def dominantMode (s : HyperEigenSpectrum) : EigenMode :=
let raw := s.bind.toArray
-- find raw index of maximum
let maxIdx := argmax raw
-- map to EigenMode
match maxIdx with
| 0 => .voidHierarchy
| 1 => .scarRoughness
| 2 => .densitySpectrum
| 3 => .lacunarity
| 4 => .topoComponents
| 5 => .topoTunnels
| 6 => .topoVoids
| 7 => .percolation
| 8 => .curvature
| 9 => .coupling
| _ => .residual
-- ═══════════════════════════════════════════════════════════════════
-- §6 Regime transition detection
-- ═══════════════════════════════════════════════════════════════════
/--
Compare two spectra at consecutive observer scales.
Returns `true` if the dominant mode changed or λ_dom shifted by >25%.
-/
def hasRegimeShift (s1 s2 : HyperEigenSpectrum) : Bool :=
let modeChanged := dominantMode s1 != dominantMode s2
let dom1 := s1.lambdaDom
let dom2 := s2.lambdaDom
let diff := if dom2.val ≥ dom1.val then dom2.val - dom1.val else dom1.val - dom2.val
modeChanged || diff > 16384
/--
Classify the regime transition as smooth, sharp, or discontinuous.
- Smooth: |Δλ_dom| ≤ 25%, same dominant mode
- Sharp: |Δλ_dom| > 25%, or mode changed
- Discontinuous: mode changed AND |Δλ_dom| > 50% (threshold 32768)
-/
inductive TransitionClass
| smooth -- no significant shift
| sharp -- significant but continuous shift
| discontinuous -- mode change + large λ jump (topology tear / phase boundary)
deriving Repr, BEq, DecidableEq, Inhabited
def classifyTransition (s1 s2 : HyperEigenSpectrum) : TransitionClass :=
let modeChanged := dominantMode s1 != dominantMode s2
let dom1 := s1.lambdaDom
let dom2 := s2.lambdaDom
let diff := if dom2.val ≥ dom1.val then dom2.val - dom1.val else dom1.val - dom2.val
if modeChanged && diff > 32768 then .discontinuous
else if modeChanged || diff > 16384 then .sharp
else .smooth
-- ═══════════════════════════════════════════════════════════════════
-- §7 Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- Cosmic-web void region: void and percolation dominate.
def cosmicVoidBind : BindOperator :=
{ omegaM := ⟨58982⟩ -- Ω_M ≈ 0.90 (strong void)
, rK := ⟨16384⟩ -- R_K ≈ 0.25 (some boundary scar)
, dQ := ⟨13107⟩ -- D_q ≈ 0.20
, lacun := ⟨39322⟩ -- Λ ≈ 0.60 (high gap texture)
, bk0 := ⟨9830⟩ -- β₀ ≈ 0.15
, bk1 := ⟨6554⟩ -- β₁ ≈ 0.10
, bk2 := ⟨52429⟩ -- β₂ ≈ 0.80 (strong enclosed-void topology)
, perc := ⟨45875⟩ -- P ≈ 0.70 (connected filament web)
, curv := ⟨9830⟩ -- C ≈ 0.15
, eta := ⟨3277⟩ -- η ≈ 0.05 (low coupling)
, eps := ⟨1638⟩ } -- ε ≈ 0.025
def cosmicVoidSpectrum : HyperEigenSpectrum :=
fromBind cosmicVoidBind ⟨0⟩
#eval cosmicVoidSpectrum.lambdaDom
-- expected: the highest of the void/percolation/topology scores ≈ ⟨58982⟩
#eval (dominantMode cosmicVoidSpectrum).label
-- expected: "Ω_M: Menger void hierarchy"
-- Fracture boundary: scar roughness and stress dominate.
def fractureBind : BindOperator :=
{ omegaM := ⟨9830⟩ -- low void
, rK := ⟨62259⟩ -- R_K ≈ 0.95 (strong boundary scar)
, dQ := ⟨26214⟩ -- D_q ≈ 0.40
, lacun := ⟨13107⟩
, bk0 := ⟨6554⟩
, bk1 := ⟨29491⟩ -- β₁ ≈ 0.45 (tunnel cracks)
, bk2 := ⟨3277⟩
, perc := ⟨16384⟩
, curv := ⟨52429⟩ -- C ≈ 0.80 (high curvature at fracture)
, eta := ⟨45875⟩ -- η ≈ 0.70 (strong stress coupling)
, eps := ⟨6554⟩ }
def fractureSpectrum : HyperEigenSpectrum :=
fromBind fractureBind ⟨65536⟩
#eval (dominantMode fractureSpectrum).label
-- expected: "R_K: Koch boundary scar"
-- Regime transition between the two.
#eval classifyTransition cosmicVoidSpectrum fractureSpectrum
-- expected: TransitionClass.discontinuous (dominant mode changed, large Δλ)
-- Lift from a perfect EigenmassOperator.
#eval (fromEigenmassOperator fullyAdmittingOperator).dominantLabel
-- expected: one of the mode names (all equal weights → first by sort stability)
end Semantics.HCMMR.Kernels.HyperEigenSpectrum

View file

@ -0,0 +1,160 @@
/-
PrimeGearCache.lean — Prime exponent compositional caching kernel.
Instead of computing every step n from scratch, factor n = Π p^{v_p(n)} and
compose from cached prime-step receipts. Δ_n = g_field(p_n) × Π (Δ_p)^{v_p(n)}.
Composites are derived, not recomputed.
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.PrimeGearCache
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
structure PrimeGearEntry where
prime : Q16_16
delta : Q16_16
fieldResponse : Q16_16
fammScar : Q16_16
chiralityReceipt : Q16_16
residual : Q16_16
receiptRoot : String
deriving Repr, BEq, DecidableEq, Inhabited
structure PrimeCache where
entries : List PrimeGearEntry
primesKnown : Nat
deriving Repr, BEq, DecidableEq, Inhabited
def factorize (n : Nat) : List (Nat × Nat) := Id.run do
let mut result : List (Nat × Nat) := []
let mut m := n
let mut d := 2
while d * d ≤ m do
if m % d == 0 then
let mut exp := 0
while m % d == 0 do
m := m / d
exp := exp + 1
result := (d, exp) :: result
d := d + 1
if m > 1 then
result := (m, 1) :: result
return result.reverse
def findEntry (cache : PrimeCache) (p : Q16_16) : Option PrimeGearEntry :=
cache.entries.find? (fun e => e.prime == p)
def q16Pow : Q16_16 → Nat → Q16_16
| _, 0 => Q16_16.one
| base, n+1 => base * q16Pow base n
def composeFromPrimes (n : Nat) (cache : PrimeCache) : Q16_16 :=
let factors := factorize n
match factors with
| [] => Q16_16.one
| _ =>
let f (acc : Q16_16) (pair : Nat × Nat) : Q16_16 :=
let (p, exp) := pair
let pQ := Q16_16.ofInt (Int.ofNat p)
match findEntry cache pQ with
| none => acc
| some entry => acc * q16Pow entry.delta exp
factors.foldl f Q16_16.one
def isCompositeCached (n : Nat) (cache : PrimeCache) : Bool :=
let factors := factorize n
factors.all (fun (p, _) =>
let pQ := Q16_16.ofInt (Int.ofNat p)
(findEntry cache pQ).isSome)
def cachePrimeStep (cache : PrimeCache) (entry : PrimeGearEntry) : PrimeCache :=
let trimmed := cache.entries.filter (fun e => e.prime != entry.prime)
{ entries := entry :: trimmed
, primesKnown := if (findEntry cache entry.prime).isSome then cache.primesKnown else cache.primesKnown + 1
}
def primeCacheGate : Gate :=
{ name := "PrimeGearCache"
, required := false
, score := Q16_16.one
, verdict := GateVerdict.admit
}
def emptyCache : PrimeCache :=
{ entries := [], primesKnown := 0 }
def fixtureEntry2 : PrimeGearEntry :=
{ prime := Q16_16.two
, delta := Q16_16.ofInt 1
, fieldResponse := Q16_16.ofInt 2
, fammScar := Q16_16.zero
, chiralityReceipt := Q16_16.one
, residual := Q16_16.zero
, receiptRoot := "deadbeef00000000000000000000000000000000000000000000000000000000"
}
def fixtureEntry3 : PrimeGearEntry :=
{ prime := Q16_16.ofInt 3
, delta := Q16_16.ofInt 6
, fieldResponse := Q16_16.ofInt 3
, fammScar := Q16_16.one
, chiralityReceipt := Q16_16.negOne
, residual := Q16_16.epsilon
, receiptRoot := "cafebabe00000000000000000000000000000000000000000000000000000000"
}
def fixtureEntry5 : PrimeGearEntry :=
{ prime := Q16_16.ofInt 5
, delta := Q16_16.ofInt 15
, fieldResponse := Q16_16.ofInt 5
, fammScar := Q16_16.zero
, chiralityReceipt := Q16_16.one
, residual := Q16_16.epsilon
, receiptRoot := "feedface00000000000000000000000000000000000000000000000000000000"
}
def fixtureCache : PrimeCache :=
cachePrimeStep (cachePrimeStep emptyCache fixtureEntry2) fixtureEntry3
def fixtureCache3 : PrimeCache :=
cachePrimeStep (cachePrimeStep (cachePrimeStep emptyCache fixtureEntry2) fixtureEntry3) fixtureEntry5
theorem cache_prime_increments_known : (cachePrimeStep emptyCache fixtureEntry2).primesKnown = 1 := by
native_decide
theorem cache_duplicate_does_not_increment : (cachePrimeStep (cachePrimeStep emptyCache fixtureEntry2) fixtureEntry2).primesKnown = 1 := by
native_decide
theorem gate_name_correct : primeCacheGate.name = "PrimeGearCache" := by
rfl
theorem fixtureCache_primes_known_two : fixtureCache.primesKnown = 2 := by
native_decide
theorem q16Pow_zero_exp : q16Pow (Q16_16.ofInt 5) 0 = Q16_16.one := by
native_decide
theorem q16Pow_one_exp : q16Pow (Q16_16.ofInt 3) 1 = Q16_16.ofInt 3 := by
native_decide
theorem empty_cache_no_entry : (findEntry emptyCache Q16_16.two).isSome = false := by
native_decide
#eval! factorize 1
#eval! factorize 7
#eval! factorize 12
#eval! factorize 30
#eval! factorize 17
#eval! isCompositeCached 6 fixtureCache3
#eval! isCompositeCached 5 fixtureCache3
#eval! composeFromPrimes 2 fixtureCache3
#eval! composeFromPrimes 6 fixtureCache3
#eval cachePrimeStep emptyCache fixtureEntry2
#eval fixtureCache3
#eval primeCacheGate
end Semantics.HCMMR.Kernels.PrimeGearCache

View file

@ -0,0 +1,151 @@
/-
RecamanFieldStep.lean — Recamán signed-step reflex kernel for HCMMR field traversal.
Recamán sequence: a_0=0, a_n = a_{n-1}-n if positive and unused, else a_{n-1}+n.
HCMMR mapping: try negative/Underverse step → if admissible and unoccupied → commit;
else reflect into positive ladder. Each step is a semicircle in circle-packing:
center m_n = (a_{n-1}+a_n)/2, radius r_n = n/2, sign s_n ∈ {+,-}.
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.RecamanFieldStep
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
structure RecamanStep where
stepIndex : Nat
currentState : Q16_16
nextState : Q16_16
attemptedNegative : Bool
reflectedPositive : Bool
residual : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
structure RecamanArc where
center : Q16_16
radius : Q16_16
sign : Q16_16
arcLength : Q16_16
curvature : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
def recamanFieldStep (currentState : Q16_16) (stepIndex : Nat) (visitedSet : List Q16_16) (fieldGate : Gate) : RecamanStep :=
let n := Q16_16.ofInt (Int.ofNat stepIndex)
let negativeCandidate := currentState - n
let negativeValid := Q16_16.gt negativeCandidate Q16_16.zero
let negativeUnused := ¬ visitedSet.any (fun v => v == negativeCandidate)
let gateAdmits := fieldGate.verdict == GateVerdict.admit
if negativeValid && negativeUnused && gateAdmits then
{ stepIndex := stepIndex
, currentState := currentState
, nextState := negativeCandidate
, attemptedNegative := true
, reflectedPositive := false
, residual := Q16_16.zero
}
else
let positiveCandidate := currentState + n
{ stepIndex := stepIndex
, currentState := currentState
, nextState := positiveCandidate
, attemptedNegative := true
, reflectedPositive := true
, residual := if negativeValid && negativeUnused then fieldGate.score else Q16_16.one
}
def arcFromStep (step : RecamanStep) : RecamanArc :=
let n := Q16_16.ofInt (Int.ofNat step.stepIndex)
let center := (step.currentState + step.nextState) * Q16_16.recip (Q16_16.two)
let radius := n * Q16_16.recip (Q16_16.two)
let s := if step.reflectedPositive then Q16_16.one else Q16_16.negOne
let piApprox : Q16_16 := ⟨205944⟩
let arclen := piApprox * radius
let curv := if radius.val == 0 then Q16_16.maxVal else Q16_16.recip radius
{ center := center
, radius := radius
, sign := s
, arcLength := arclen
, curvature := curv
}
def circleIntersectionCheck (a b : RecamanArc) : Bool :=
let d := Q16_16.abs (a.center - b.center)
let sumRadii := a.radius + b.radius
let diffRadii := Q16_16.abs (a.radius - b.radius)
let withinOuter := Q16_16.le d sumRadii
let outsideInner := Q16_16.ge d diffRadii
withinOuter && outsideInner
def cumulativeArcLength (steps : List RecamanStep) : Q16_16 :=
let piApprox : Q16_16 := ⟨205944⟩
let f (acc : Q16_16) (step : RecamanStep) : Q16_16 :=
let n := Q16_16.ofInt (Int.ofNat step.stepIndex)
let r := n * Q16_16.recip (Q16_16.two)
acc + piApprox * r
steps.foldl f Q16_16.zero
def recamanGateAdmit : Gate :=
{ name := "RecamanFieldStep"
, required := false
, score := Q16_16.one
, verdict := GateVerdict.admit
}
def fixtureStep1 : RecamanStep :=
{ stepIndex := 1
, currentState := Q16_16.zero
, nextState := Q16_16.one
, attemptedNegative := false
, reflectedPositive := false
, residual := Q16_16.zero
}
def fixtureStep2 : RecamanStep :=
{ stepIndex := 2
, currentState := Q16_16.one
, nextState := Q16_16.ofInt 3
, attemptedNegative := true
, reflectedPositive := true
, residual := Q16_16.one
}
def fixtureStep3 : RecamanStep :=
{ stepIndex := 3
, currentState := Q16_16.ofInt 3
, nextState := Q16_16.ofInt 6
, attemptedNegative := true
, reflectedPositive := true
, residual := Q16_16.one
}
def fixtureArc1 : RecamanArc := arcFromStep fixtureStep1
def fixtureArc2 : RecamanArc := arcFromStep fixtureStep2
def fixtureVisited : List Q16_16 := [Q16_16.one, Q16_16.ofInt 3]
def fixtureGate : Gate :=
{ name := "testFieldGate", required := true, score := Q16_16.one, verdict := GateVerdict.admit }
theorem recaman_gate_name_correct : recamanGateAdmit.name = "RecamanFieldStep" := by
rfl
theorem recaman_gate_verdict_admits : recamanGateAdmit.verdict = GateVerdict.admit := by
rfl
theorem fixture_step1_index_one : fixtureStep1.stepIndex = 1 := by rfl
theorem fixture_step2_index_two : fixtureStep2.stepIndex = 2 := by rfl
theorem fixture_step1_reflected_false : fixtureStep1.reflectedPositive = false := by rfl
theorem fixture_step2_reflected_true : fixtureStep2.reflectedPositive = true := by rfl
#eval recamanFieldStep Q16_16.zero 1 [] fixtureGate
#eval recamanFieldStep Q16_16.one 2 fixtureVisited fixtureGate
#eval fixtureArc1
#eval fixtureArc2
#eval circleIntersectionCheck fixtureArc1 fixtureArc2
#eval cumulativeArcLength [fixtureStep1, fixtureStep2, fixtureStep3]
#eval cumulativeArcLength []
#eval recamanGateAdmit
end Semantics.HCMMR.Kernels.RecamanFieldStep

View file

@ -0,0 +1,218 @@
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Kernels.SNRAnomalyDetector
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
inductive SignalPattern where
| narrowbandSpike
| broadbandRise
| dopplerDrift
| flickerTransient
| periodicPulsar
| unknownAnomaly
deriving Repr, BEq, DecidableEq, Inhabited
instance : ToString SignalPattern where
toString
| SignalPattern.narrowbandSpike => "narrowbandSpike"
| SignalPattern.broadbandRise => "broadbandRise"
| SignalPattern.dopplerDrift => "dopplerDrift"
| SignalPattern.flickerTransient => "flickerTransient"
| SignalPattern.periodicPulsar => "periodicPulsar"
| SignalPattern.unknownAnomaly => "unknownAnomaly"
inductive SNRZone where
| signalZone
| noiseZone
| ambiguousZone
deriving Repr, BEq, DecidableEq, Inhabited
structure SNRBin where
frequencyHz : Q16_16
bandwidthHz : Q16_16
signalPower : Q16_16
noiseFloor : Q16_16
snrValue : Q16_16
integrationTime : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
def computeSNR (signal noise : Q16_16) : Q16_16 :=
if noise.val == 0 then Q16_16.zero
else Q16_16.div signal noise
def classifySNRZone (snr tauSignal tauNoise : Q16_16) : SNRZone :=
if Q16_16.le tauSignal snr then SNRZone.signalZone
else if Q16_16.le snr tauNoise then SNRZone.noiseZone
else SNRZone.ambiguousZone
def isNarrowband (bin : SNRBin) : Bool :=
let frac := Q16_16.div bin.bandwidthHz bin.frequencyHz
Q16_16.lt frac (Q16_16.ofRatio 1 100)
def isBroadband (bin : SNRBin) : Bool :=
let frac := Q16_16.div bin.bandwidthHz bin.frequencyHz
Q16_16.lt (Q16_16.ofRatio 10 100) frac
def classifyPattern (bins : List SNRBin) (tauSignal : Q16_16) : SignalPattern :=
let narrowSpikes := bins.filter fun b =>
Q16_16.le tauSignal b.snrValue && isNarrowband b
let broadRises := bins.filter fun b =>
Q16_16.le tauSignal b.snrValue && isBroadband b
if narrowSpikes.length > 0 then
if narrowSpikes.length == 1 then SignalPattern.narrowbandSpike
else SignalPattern.periodicPulsar
else if broadRises.length > 0 then
SignalPattern.broadbandRise
else if bins.any fun b => Q16_16.le tauSignal b.snrValue then
SignalPattern.unknownAnomaly
else
SignalPattern.flickerTransient
def anomalyScore (bin : SNRBin) (baselineSNR : Q16_16) : Q16_16 :=
let delta := Q16_16.abs (Q16_16.sub bin.snrValue baselineSNR)
if delta.val == 0 then Q16_16.zero
else Q16_16.log2 (Q16_16.add Q16_16.one delta)
def narrowbandSpikeFixture : SNRBin :=
{ frequencyHz := (Q16_16.ofInt 1420)
, bandwidthHz := (Q16_16.ofInt 1)
, signalPower := (Q16_16.ofInt 100)
, noiseFloor := Q16_16.one
, snrValue := (Q16_16.ofInt 100)
, integrationTime := (Q16_16.ofInt 60)
}
def broadbandRiseFixture : SNRBin :=
{ frequencyHz := (Q16_16.ofInt 1500)
, bandwidthHz := (Q16_16.ofInt 500)
, signalPower := (Q16_16.ofInt 50)
, noiseFloor := (Q16_16.ofInt 5)
, snrValue := (Q16_16.ofInt 10)
, integrationTime := (Q16_16.ofInt 30)
}
def noiseFloorFixture : SNRBin :=
{ frequencyHz := (Q16_16.ofInt 1000)
, bandwidthHz := (Q16_16.ofInt 10)
, signalPower := Q16_16.one
, noiseFloor := (Q16_16.ofInt 10)
, snrValue := Q16_16.ofRatio 1 10
, integrationTime := (Q16_16.ofInt 10)
}
def multiBinFixture : List SNRBin :=
[ narrowbandSpikeFixture, broadbandRiseFixture, noiseFloorFixture ]
def snrDetectionGate (bin : SNRBin) (tauSignal tauNoise : Q16_16) : Gate :=
let zone := classifySNRZone bin.snrValue tauSignal tauNoise
match zone with
| SNRZone.signalZone =>
if isNarrowband bin then
{ name := "SNRDetection:narrowbandSpike"
, required := true
, score := Q16_16.one
, verdict := GateVerdict.admit
}
else
{ name := "SNRDetection:broadbandRise"
, required := true
, score := Q16_16.ofRatio 5 10
, verdict := GateVerdict.hold
}
| SNRZone.ambiguousZone =>
{ name := "SNRDetection:ambiguous"
, required := true
, score := Q16_16.ofRatio 3 10
, verdict := GateVerdict.hold
}
| SNRZone.noiseZone =>
{ name := "SNRDetection:noise"
, required := true
, score := Q16_16.zero
, verdict := GateVerdict.reject
}
def emitAnomalyReceipt (bin : SNRBin) (pattern : SignalPattern) (ts : Nat) : DiagnosticReceipt :=
let route := match pattern with
| SignalPattern.narrowbandSpike => "reobserve_drift_correct"
| SignalPattern.broadbandRise => "thermal_environmental_check"
| SignalPattern.dopplerDrift => "doppler_compensation"
| SignalPattern.flickerTransient => "rfi_exclusion"
| SignalPattern.periodicPulsar => "periodicity_followup"
| SignalPattern.unknownAnomaly => "Underverse"
{ object := "freq_bin"
, failedGate := "SNRDetection:anomaly"
, alternateRoute := route
, timestamp := ts
, residual :=
{ domain := "snr_anomaly"
, value := anomalyScore bin Q16_16.one
, source := "SNRAnomalyDetector"
}
}
def findStrongestSpike (bins : List SNRBin) : SNRBin :=
bins.foldl (fun best b =>
if Q16_16.lt best.snrValue b.snrValue then b else best)
{ frequencyHz := Q16_16.zero, bandwidthHz := Q16_16.one
, signalPower := Q16_16.zero, noiseFloor := Q16_16.one
, snrValue := Q16_16.zero, integrationTime := Q16_16.one
}
def countDetections (bins : List SNRBin) (tauSignal : Q16_16) : Nat :=
(bins.filter fun b => Q16_16.le tauSignal b.snrValue).length
theorem narrowband_spike_admits :
(snrDetectionGate narrowbandSpikeFixture (Q16_16.ofInt 10) Q16_16.one).verdict = GateVerdict.admit := by
native_decide
theorem noise_floor_rejects :
(snrDetectionGate noiseFloorFixture (Q16_16.ofInt 10) Q16_16.one).verdict = GateVerdict.reject := by
native_decide
theorem broadband_rise_holds :
(snrDetectionGate broadbandRiseFixture (Q16_16.ofInt 5) Q16_16.one).verdict = GateVerdict.hold := by
native_decide
theorem narrowband_is_narrowband :
isNarrowband narrowbandSpikeFixture = true := by
native_decide
theorem anomaly_score_self_delta :
anomalyScore narrowbandSpikeFixture narrowbandSpikeFixture.snrValue = Q16_16.zero := by
native_decide
theorem detection_count_multi_bin :
countDetections multiBinFixture (Q16_16.ofInt 5) = 2 := by
native_decide
#eval computeSNR (Q16_16.ofInt 200) (Q16_16.ofInt 20)
#eval computeSNR (Q16_16.ofInt 5) Q16_16.zero
#eval classifySNRZone narrowbandSpikeFixture.snrValue (Q16_16.ofInt 10) Q16_16.one
#eval classifySNRZone broadbandRiseFixture.snrValue (Q16_16.ofInt 20) (Q16_16.ofInt 5)
#eval classifySNRZone noiseFloorFixture.snrValue (Q16_16.ofInt 10) Q16_16.one
#eval isNarrowband narrowbandSpikeFixture
#eval isBroadband broadbandRiseFixture
#eval classifyPattern [narrowbandSpikeFixture] (Q16_16.ofInt 10)
#eval classifyPattern [broadbandRiseFixture] (Q16_16.ofInt 5)
#eval classifyPattern multiBinFixture (Q16_16.ofInt 10)
#eval anomalyScore narrowbandSpikeFixture Q16_16.one
#eval anomalyScore noiseFloorFixture Q16_16.one
#eval snrDetectionGate narrowbandSpikeFixture (Q16_16.ofInt 10) Q16_16.one
#eval snrDetectionGate broadbandRiseFixture (Q16_16.ofInt 5) (Q16_16.ofInt 5)
#eval snrDetectionGate noiseFloorFixture (Q16_16.ofInt 10) Q16_16.one
#eval emitAnomalyReceipt narrowbandSpikeFixture SignalPattern.narrowbandSpike 42
#eval findStrongestSpike multiBinFixture
#eval countDetections multiBinFixture (Q16_16.ofInt 5)
end Semantics.HCMMR.Kernels.SNRAnomalyDetector

View file

@ -0,0 +1,343 @@
/-
HCMMR Law14 — Motion Recovery.
Tests whether a 16D object can be projected into a classical trajectory.
The pass condition is ε_motion = ||m·ẍ - F|| → 0 in the Newtonian limit.
When residuals are small, the HCMMR manifold gear-reduces to classical
Newtonian/Lagrangian mechanics.
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law14
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
set_option maxRecDepth 20000
-- ═══════════════════════════════════════════════════════════════════
-- §1 Projected Trajectory
-- ═══════════════════════════════════════════════════════════════════
structure TrajectoryPoint where
positionX : Q16_16
positionY : Q16_16
positionZ : Q16_16
velocityX : Q16_16
velocityY : Q16_16
velocityZ : Q16_16
accelX : Q16_16
accelY : Q16_16
accelZ : Q16_16
mass : Q16_16
forceX : Q16_16
forceY : Q16_16
forceZ : Q16_16
timestamp : Nat
deriving Repr, BEq, DecidableEq, Inhabited
/--
Finite-difference velocity: v = (p1 - p0) / dt
Applied per spatial dimension.
-/
def computeVelocity (pos0 pos1 dt : Q16_16) : Q16_16 :=
Q16_16.div (Q16_16.sub pos1 pos0) dt
/--
Finite-difference acceleration: a = (v1 - v0) / dt
Applied per spatial dimension.
-/
def computeAcceleration (vel0 vel1 dt : Q16_16) : Q16_16 :=
Q16_16.div (Q16_16.sub vel1 vel0) dt
-- ═══════════════════════════════════════════════════════════════════
-- §2 Newtonian Recovery Tests
-- ═══════════════════════════════════════════════════════════════════
/--
ε_Fma = ||F - m·a|| — Newton's second-law residual.
Returns the per-dimension maximum across x, y, z.
-/
def newtonSecondLawResidual (tp : TrajectoryPoint) : Q16_16 :=
let maX := Q16_16.mul tp.mass tp.accelX
let maY := Q16_16.mul tp.mass tp.accelY
let maZ := Q16_16.mul tp.mass tp.accelZ
let resX := Q16_16.abs (Q16_16.sub tp.forceX maX)
let resY := Q16_16.abs (Q16_16.sub tp.forceY maY)
let resZ := Q16_16.abs (Q16_16.sub tp.forceZ maZ)
Q16_16.max (Q16_16.max resX resY) resZ
/--
ε_pmv = ||p - m·v|| — momentum residual.
Supplied momentum components are compared against m·v in each dimension.
Returns the maximum residual.
-/
def momentumResidual (px py pz mass vx vy vz : Q16_16) : Q16_16 :=
let mvx := Q16_16.mul mass vx
let mvy := Q16_16.mul mass vy
let mvz := Q16_16.mul mass vz
let resX := Q16_16.abs (Q16_16.sub px mvx)
let resY := Q16_16.abs (Q16_16.sub py mvy)
let resZ := Q16_16.abs (Q16_16.sub pz mvz)
Q16_16.max (Q16_16.max resX resY) resZ
/--
ε_Ek = ||E_k - ½·m·|v|²|| — kinetic-energy residual.
-/
def kineticEnergyResidual (ek mass vx vy vz : Q16_16) : Q16_16 :=
let v2 := Q16_16.add (Q16_16.add (Q16_16.mul vx vx) (Q16_16.mul vy vy)) (Q16_16.mul vz vz)
let halfMV2 := Q16_16.mul (Q16_16.mul (Q16_16.ofRatio 1 2) mass) v2
Q16_16.abs (Q16_16.sub ek halfMV2)
-- ═══════════════════════════════════════════════════════════════════
-- §3 Lagrangian Recovery
-- ═══════════════════════════════════════════════════════════════════
structure LagrangianState where
q : Q16_16
qdot : Q16_16
mass : Q16_16
kinetic : Q16_16
potential : Q16_16
lagrangian : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
ε_EL = ||d/dt(∂L/∂q̇) - ∂L/∂q|| — discrete Euler-Lagrange residual.
Approximates d/dt(m·q̇) ≈ (p₁-p₀)/dt and ∂V/∂q ≈ (V₁-V₀)/(q₁-q₀).
The E-L equation demands dp/dt + ∂V/∂q = 0.
-/
def eulerLagrangeResidual (s0 s1 : LagrangianState) (dt : Q16_16) : Q16_16 :=
let p0 := Q16_16.mul s0.mass s0.qdot
let p1 := Q16_16.mul s1.mass s1.qdot
let dp_dt := Q16_16.div (Q16_16.sub p1 p0) dt
let dV_dq := if s0.q == s1.q then Q16_16.zero
else Q16_16.div (Q16_16.sub s1.potential s0.potential) (Q16_16.sub s1.q s0.q)
Q16_16.abs (Q16_16.add dp_dt dV_dq)
/--
ε_S = ||δS|| — first variation of the action.
Discrete approximation: δS ≈ (∂L/∂q)·δq·dt.
Uses finite-difference ∂L/∂q between two consecutive states.
-/
def actionResidual (s0 s1 : LagrangianState) (dt δq : Q16_16) : Q16_16 :=
if s0.q == s1.q then Q16_16.zero
else
let dL_dq := Q16_16.div (Q16_16.sub s1.lagrangian s0.lagrangian) (Q16_16.sub s1.q s0.q)
let deltaS := Q16_16.mul (Q16_16.mul dL_dq δq) dt
Q16_16.abs deltaS
-- ═══════════════════════════════════════════════════════════════════
-- §4 Motion Recovery Gate
-- ═══════════════════════════════════════════════════════════════════
/--
Motion-recovery gate: admits iff all classical residuals are within
their respective thresholds. Otherwise holds (motion is not classical;
it may be quantum, relativistic, or intrinsically 16D).
-/
def motionRecoveryGate (epsFma epsEL epsS tauFma tauEL tauS : Q16_16) : Gate :=
let passed := Q16_16.le epsFma tauFma && Q16_16.le epsEL tauEL && Q16_16.le epsS tauS
{ name := "MotionRecovery"
, required := true
, score := if passed then Q16_16.one else Q16_16.zero
, verdict := if passed then GateVerdict.admit else GateVerdict.hold
}
/--
Emit a diagnostic receipt for every equation whose residual exceeds its
threshold. Each receipt records the failed equation, residual value,
and a suggested alternate route.
-/
def motionDiagnostic (epsFma epsEL epsS epsPmv epsEk tauFma tauEL tauS tauPmv tauEk : Q16_16)
(objId : String) (ts : Nat) : List DiagnosticReceipt :=
let mk (failed : String) (res : Q16_16) (route : String) : DiagnosticReceipt :=
{ object := objId, failedGate := failed,
residual := ⟨failed, res, "MotionRecovery"⟩,
alternateRoute := route, timestamp := ts }
let check (cond : Bool) (failed : String) (res : Q16_16) (route : String)
(acc : List DiagnosticReceipt) : List DiagnosticReceipt :=
if cond then acc else mk failed res route :: acc
let receipts : List DiagnosticReceipt := []
let receipts := check (Q16_16.le epsFma tauFma) "F=ma" epsFma "relativistic_correction" receipts
let receipts := check (Q16_16.le epsEL tauEL) "δS=0" epsEL "quantum_regime" receipts
let receipts := check (Q16_16.le epsS tauS) "δS=0" epsS "quantum_regime" receipts
let receipts := check (Q16_16.le epsPmv tauPmv) "p=mv" epsPmv "16D_direct" receipts
let receipts := check (Q16_16.le epsEk tauEk) "E=½mv²" epsEk "relativistic_correction" receipts
receipts.reverse
-- ═══════════════════════════════════════════════════════════════════
-- §5 Gear Reduction Check
-- ═══════════════════════════════════════════════════════════════════
/--
Root-sum-square accumulation of projection residuals across the gear
reduction chain: 16D → 8D → 4D → 3D → trajectory.
Each step may introduce a dimensional mismatch ε; the total accumulated
error is the RSS of all steps.
-/
def gearReduceResidual (r16to8 r8to4 r4to3 r3ToTrajectory : Q16_16) : Q16_16 :=
let r1 := Q16_16.mul r16to8 r16to8
let r2 := Q16_16.mul r8to4 r8to4
let r3 := Q16_16.mul r4to3 r4to3
let r4 := Q16_16.mul r3ToTrajectory r3ToTrajectory
Q16_16.sqrt (Q16_16.add (Q16_16.add (Q16_16.add r1 r2) r3) r4)
-- ═══════════════════════════════════════════════════════════════════
-- §6 Fixtures
-- ═══════════════════════════════════════════════════════════════════
/--
Clean Newtonian trajectory: F = m·a holds exactly in all three
dimensions. mass = 2, a = (1,2,3), F = (2,4,6).
-/
def cleanNewtonFixture : TrajectoryPoint :=
{ positionX := Q16_16.zero, positionY := Q16_16.zero, positionZ := Q16_16.zero
, velocityX := Q16_16.zero, velocityY := Q16_16.zero, velocityZ := Q16_16.zero
, accelX := Q16_16.one, accelY := Q16_16.two, accelZ := (Q16_16.ofInt 3)
, mass := Q16_16.two
, forceX := Q16_16.two, forceY := (Q16_16.ofInt 4), forceZ := (Q16_16.ofInt 6)
, timestamp := 0
}
/--
Violating trajectory: F ≠ m·a on the x-axis.
Same mass and acceleration, but x-force is off by 1.
-/
def violatingTrajectoryFixture : TrajectoryPoint :=
{ cleanNewtonFixture with
forceX := Q16_16.add cleanNewtonFixture.forceX Q16_16.one
timestamp := 1
}
/--
Clean Lagrangian pair: two consecutive states of a uniform-motion
system where V is constant and q̇ is constant, so E-L holds trivially.
-/
def cleanLagrangianFixture : LagrangianState × LagrangianState :=
let s0 : LagrangianState :=
{ q := Q16_16.ofInt 0, qdot := Q16_16.one, mass := Q16_16.one
, kinetic := Q16_16.ofRatio 1 2, potential := Q16_16.ofInt 5
, lagrangian := Q16_16.sub (Q16_16.ofRatio 1 2) (Q16_16.ofInt 5) }
let s1 : LagrangianState :=
{ q := Q16_16.one, qdot := Q16_16.one, mass := Q16_16.one
, kinetic := Q16_16.ofRatio 1 2, potential := Q16_16.ofInt 5
, lagrangian := Q16_16.sub (Q16_16.ofRatio 1 2) (Q16_16.ofInt 5) }
(s0, s1)
/--
Free-particle fixture: L = ½ m v² with V = 0.
Two consecutive states with constant velocity; E-L and action both vanish.
-/
def freeParticleFixture : LagrangianState × LagrangianState :=
let s0 : LagrangianState :=
{ q := Q16_16.ofInt 0, qdot := Q16_16.one, mass := Q16_16.one
, kinetic := Q16_16.ofRatio 1 2, potential := Q16_16.zero
, lagrangian := Q16_16.ofRatio 1 2 }
let s1 : LagrangianState :=
{ q := Q16_16.one, qdot := Q16_16.one, mass := Q16_16.one
, kinetic := Q16_16.ofRatio 1 2, potential := Q16_16.zero
, lagrangian := Q16_16.ofRatio 1 2 }
(s0, s1)
-- ═══════════════════════════════════════════════════════════════════
-- §7 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
The clean Newtonian fixture passes the motion-recovery gate when the
other residual channels are set to zero.
-/
theorem newton_admits_clean :
motionRecoveryGate (newtonSecondLawResidual cleanNewtonFixture)
Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero
= { name := "MotionRecovery", required := true, score := Q16_16.one,
verdict := GateVerdict.admit } := by
native_decide
/--
The free-particle Lagrangian passes the motion-recovery gate.
-/
theorem free_particle_admits :
let (s0, s1) := freeParticleFixture
let dt := Q16_16.one
let tau : Q16_16 := Q16_16.ofRatio 1 100
motionRecoveryGate Q16_16.zero (eulerLagrangeResidual s0 s1 dt)
(actionResidual s0 s1 dt tau) Q16_16.zero tau tau
= { name := "MotionRecovery", required := true, score := Q16_16.one,
verdict := GateVerdict.admit } := by
native_decide
/--
When momentum is computed from mass and velocity (p = m·v), the
momentum residual is identically zero.
-/
theorem momentum_identity_clean :
momentumResidual Q16_16.two Q16_16.zero Q16_16.zero
Q16_16.two Q16_16.one Q16_16.zero Q16_16.zero
= Q16_16.zero := by
native_decide
/--
When E_k is computed exactly from ½·m·|v|², the kinetic-energy
residual is zero.
-/
theorem kinetic_energy_clean :
kineticEnergyResidual (Q16_16.ofInt 1) Q16_16.two
Q16_16.one Q16_16.zero Q16_16.zero
= Q16_16.zero := by
native_decide
/--
The violating fixture produces a nonzero Newton residual.
-/
theorem newton_violating_residual_pos :
(newtonSecondLawResidual violatingTrajectoryFixture).val > Q16_16.zero.val := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §8 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
#eval computeVelocity Q16_16.zero (Q16_16.ofInt 10) (Q16_16.ofInt 2)
#eval computeAcceleration Q16_16.zero (Q16_16.ofInt 5) (Q16_16.one)
#eval newtonSecondLawResidual cleanNewtonFixture
#eval newtonSecondLawResidual violatingTrajectoryFixture
#eval momentumResidual (Q16_16.ofInt 10) Q16_16.zero Q16_16.zero
(Q16_16.ofInt 2) (Q16_16.ofInt 5) Q16_16.zero Q16_16.zero
#eval momentumResidual Q16_16.two Q16_16.zero Q16_16.zero
Q16_16.two Q16_16.one Q16_16.zero Q16_16.zero
#eval kineticEnergyResidual (Q16_16.ofInt 25)
(Q16_16.ofInt 2) (Q16_16.ofInt 5) Q16_16.zero Q16_16.zero
#eval kineticEnergyResidual (Q16_16.mul (Q16_16.ofRatio 1 2)
(Q16_16.mul Q16_16.two (Q16_16.mul Q16_16.one Q16_16.one)))
Q16_16.two Q16_16.one Q16_16.zero Q16_16.zero
#eval eulerLagrangeResidual cleanLagrangianFixture.1 cleanLagrangianFixture.2 Q16_16.one
#eval actionResidual cleanLagrangianFixture.1 cleanLagrangianFixture.2
Q16_16.one (Q16_16.ofRatio 1 100)
#eval eulerLagrangeResidual freeParticleFixture.1 freeParticleFixture.2 Q16_16.one
#eval actionResidual freeParticleFixture.1 freeParticleFixture.2
Q16_16.one (Q16_16.ofRatio 1 100)
#eval motionRecoveryGate (newtonSecondLawResidual cleanNewtonFixture)
Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero
#eval motionRecoveryGate (newtonSecondLawResidual violatingTrajectoryFixture)
Q16_16.zero Q16_16.zero (Q16_16.ofRatio 1 100) Q16_16.zero Q16_16.zero
#eval motionDiagnostic Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero
(Q16_16.ofRatio 1 100) (Q16_16.ofRatio 1 100) (Q16_16.ofRatio 1 100)
(Q16_16.ofRatio 1 100) (Q16_16.ofRatio 1 100) "system_3A" 42
#eval motionDiagnostic (Q16_16.ofInt 5) Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero
Q16_16.one Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero "system_3A" 42
#eval gearReduceResidual (Q16_16.ofRatio 1 1000) (Q16_16.ofRatio 2 1000)
(Q16_16.ofRatio 3 1000) (Q16_16.ofRatio 4 1000)
#eval gearReduceResidual Q16_16.zero Q16_16.zero Q16_16.zero Q16_16.zero
end Semantics.HCMMR.Law14

View file

@ -0,0 +1,278 @@
/-
Law 15E — Signal Detection Gate.
A sub-law of Field Recovery (Law 15) that gates whether a projected
electromagnetic field contains a detectable signal rather than mere noise.
The gate uses SNR ratio thresholds mapped to typed verdicts:
Signal ≥ signal_threshold → admit (candidate signal present)
Signal in ambiguous band → hold (integrate longer)
Signal ≤ noise_floor → reject (noise only)
Pattern matching adds typed classification:
- narrowband spike: high SNR in tight bin (SETI candidate, artifact)
- broadband rise: elevated background (thermal, natural, environmental)
- periodic pulsar: repeating narrowband spikes (rotating source)
- flicker/transient: short-duration spike (RFI, burst, scintillation)
- Doppler drift: frequency-shifting narrowband (moving source)
This sits after Law 15C (wave propagation) and before 15D (coupling):
First detect a signal, then test whether it couples to a source.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts, `inductive` for enumerations.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law15E
Import: Semantics.HCMMR.Core, Semantics.HCMMR.Kernels.SNRAnomalyDetector, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.HCMMR.Kernels.SNRAnomalyDetector
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law15E
open Semantics.HCMMR.Core
open Semantics.HCMMR.Kernels.SNRAnomalyDetector
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Signal Detection Configuration
-- ═══════════════════════════════════════════════════════════════════
/--
Configuration for the signal detection gate.
τ_signal: minimum SNR to claim a detection (e.g., 10x noise floor).
τ_noise: maximum SNR that is clearly noise (e.g., 3x noise floor).
minIntegrationTime: seconds needed before a hold can become admit.
dopplerSearchEnabled: enable frequency-shift pattern matching.
-/
structure SignalDetectionConfig where
tauSignal : Q16_16
tauNoise : Q16_16
minIntegrationTime : Q16_16
dopplerSearchEnabled : Bool
deriving Repr, BEq, DecidableEq, Inhabited
/--
Default SETI-style configuration: 10σ detection, 3σ noise floor,
60-second minimum integration, Doppler enabled.
-/
def setiDefaultConfig : SignalDetectionConfig :=
{ tauSignal := Q16_16.ofInt 10
, tauNoise := Q16_16.ofInt 3
, minIntegrationTime := Q16_16.ofInt 60
, dopplerSearchEnabled := true
}
/--
Quick-scan configuration: 5σ detection, shorter integration, no Doppler.
Used for RFI surveys and environment characterization.
-/
def quickScanConfig : SignalDetectionConfig :=
{ tauSignal := Q16_16.ofInt 5
, tauNoise := Q16_16.ofInt 2
, minIntegrationTime := Q16_16.ofInt 10
, dopplerSearchEnabled := false
}
-- ═══════════════════════════════════════════════════════════════════
-- §2 Signal Detection Gate
-- ═══════════════════════════════════════════════════════════════════
/--
The signal detection gate evaluates a list of SNR bins against the
configured thresholds.
Logic:
1. Find the strongest SNR bin across the spectrum
2. Classify SNR zone (signal/noise/ambiguous)
3. If signal zone: classify pattern, admit narrowband spikes, hold broadband
4. If ambiguous zone: hold, check if integration time allows upgrade
5. If noise zone: reject, no signal present
The gate is required in the multiplicative chain — no signal means
no downstream coupling test is meaningful.
-/
def signalDetectionGate (config : SignalDetectionConfig) (bins : List SNRBin) : Gate :=
let strongest := findStrongestSpike bins
let snrGate := snrDetectionGate strongest config.tauSignal config.tauNoise
let sufficientIntegration :=
Q16_16.le config.minIntegrationTime strongest.integrationTime
match snrGate.verdict with
| GateVerdict.admit =>
{ name := snrGate.name
, required := true
, score := if sufficientIntegration then Q16_16.one else Q16_16.ofRatio 8 10
, verdict := if sufficientIntegration then GateVerdict.admit else GateVerdict.hold
}
| GateVerdict.hold =>
if Q16_16.lt strongest.integrationTime config.minIntegrationTime then
{ name := "SignalDetection:integrating"
, required := true
, score := Q16_16.ofRatio 3 10
, verdict := GateVerdict.hold
}
else
snrGate
| GateVerdict.reject =>
{ name := "SignalDetection:noise"
, required := true
, score := Q16_16.zero
, verdict := GateVerdict.reject
}
-- ═══════════════════════════════════════════════════════════════════
-- §3 Multi-Pattern Detection Report
-- ═══════════════════════════════════════════════════════════════════
/--
A full detection report: the dominant pattern found, its SNR bin,
the gate verdict, and per-bin diagnostic receipts for all anomalies.
-/
structure DetectionReport where
dominantBin : SNRBin
dominantPattern : SignalPattern
gateVerdict : GateVerdict
detectionCount : Nat
receipts : List DiagnosticReceipt
deriving Repr, BEq, Inhabited
/--
Generate a full detection report from a config and bin list.
Scans all bins, identifies the dominant pattern, emits receipts for
every bin that exceeds the noise threshold.
-/
def generateDetectionReport (config : SignalDetectionConfig) (bins : List SNRBin) (ts : Nat) : DetectionReport :=
let strongest := findStrongestSpike bins
let pattern := classifyPattern bins config.tauSignal
let gate := signalDetectionGate config bins
let receipts := bins.filterMap fun b =>
if Q16_16.le config.tauSignal b.snrValue then
some (emitAnomalyReceipt b (classifyPattern [b] config.tauSignal) ts)
else
none
{ dominantBin := strongest
, dominantPattern := pattern
, gateVerdict := gate.verdict
, detectionCount := countDetections bins config.tauSignal
, receipts := receipts
}
-- ═══════════════════════════════════════════════════════════════════
-- §4 Doppler Drift Detection
-- ═══════════════════════════════════════════════════════════════════
/--
Detect Doppler drift: compare narrowband spike positions across time
windows. If the peak frequency shifts, report drift rate as Q16_16.
driftRate = (f1 - f0) / (t1 - t0), positive = approaching, negative = receding.
-/
def detectDopplerDrift (f0 f1 t0 t1 : Q16_16) : Q16_16 :=
let dt := Q16_16.sub t1 t0
if dt.val == 0 then Q16_16.zero
else Q16_16.div (Q16_16.sub f1 f0) dt
/--
Doppler detection gate: admits if a narrowband spike shows frequency drift
consistent with a moving source (non-zero, bounded rate).
-/
def dopplerGate (f0 f1 t0 t1 : Q16_16) (maxPhysicallyPlausibleDrift : Q16_16) : Gate :=
let drift := detectDopplerDrift f0 f1 t0 t1
let absDrift := Q16_16.abs drift
if absDrift.val == 0 then
{ name := "DopplerDetection:stationary"
, required := false -- optional sub-gate
, score := Q16_16.ofRatio 5 10
, verdict := GateVerdict.hold
}
else if Q16_16.le absDrift maxPhysicallyPlausibleDrift then
{ name := "DopplerDetection:drift_detected"
, required := false
, score := Q16_16.ofRatio 8 10
, verdict := GateVerdict.admit
}
else
{ name := "DopplerDetection:implausible_drift"
, required := false
, score := Q16_16.zero
, verdict := GateVerdict.reject
}
-- ═══════════════════════════════════════════════════════════════════
-- §5 Fixtures
-- ═══════════════════════════════════════════════════════════════════
def cleanSignalFixture : List SNRBin :=
[ { frequencyHz := Q16_16.ofInt 1420
, bandwidthHz := Q16_16.ofInt 1
, signalPower := Q16_16.ofInt 1000
, noiseFloor := Q16_16.one
, snrValue := Q16_16.ofInt 1000
, integrationTime := Q16_16.ofInt 120
}
]
def ambiguousSignalFixture : List SNRBin :=
[ { frequencyHz := Q16_16.ofInt 1662
, bandwidthHz := Q16_16.ofInt 5
, signalPower := Q16_16.ofInt 20
, noiseFloor := Q16_16.ofInt 5
, snrValue := Q16_16.ofInt 4
, integrationTime := Q16_16.ofInt 30
}
]
-- ═══════════════════════════════════════════════════════════════════
-- §6 Theorems
-- ═══════════════════════════════════════════════════════════════════
theorem seti_config_admits_strong_signal :
(signalDetectionGate setiDefaultConfig cleanSignalFixture).verdict = GateVerdict.admit := by
native_decide
theorem seti_config_holds_ambiguous :
(signalDetectionGate setiDefaultConfig ambiguousSignalFixture).verdict = GateVerdict.hold := by
native_decide
theorem quick_scan_admits_ambiguous_above_noise :
(signalDetectionGate quickScanConfig ambiguousSignalFixture).verdict = GateVerdict.hold := by
native_decide
theorem doppler_zero_drift_holds :
(dopplerGate (Q16_16.ofInt 1420) (Q16_16.ofInt 1420) Q16_16.zero (Q16_16.ofInt 60) (Q16_16.ofInt 10)).verdict
= GateVerdict.hold := by
native_decide
theorem doppler_valid_drift_admits :
(dopplerGate (Q16_16.ofInt 1420) (Q16_16.ofInt 1421) Q16_16.zero (Q16_16.ofInt 60) (Q16_16.ofInt 10)).verdict
= GateVerdict.admit := by
native_decide
theorem detection_report_counts_correctly :
(generateDetectionReport setiDefaultConfig cleanSignalFixture 0).detectionCount = 1 := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §7 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
#eval signalDetectionGate setiDefaultConfig cleanSignalFixture
#eval signalDetectionGate setiDefaultConfig ambiguousSignalFixture
#eval signalDetectionGate quickScanConfig ambiguousSignalFixture
#eval generateDetectionReport setiDefaultConfig cleanSignalFixture 0
#eval generateDetectionReport setiDefaultConfig ambiguousSignalFixture 1
#eval detectDopplerDrift (Q16_16.ofInt 1420) (Q16_16.ofInt 1421)
Q16_16.zero (Q16_16.ofInt 60)
#eval dopplerGate (Q16_16.ofInt 1420) (Q16_16.ofInt 1421)
Q16_16.zero (Q16_16.ofInt 60) (Q16_16.ofInt 10)
#eval dopplerGate (Q16_16.ofInt 1420) (Q16_16.ofInt 1500)
Q16_16.zero (Q16_16.ofInt 60) (Q16_16.ofInt 10)
end Semantics.HCMMR.Law15E

View file

@ -0,0 +1,630 @@
/-
Law 15 — Field Recovery
Bridges 16D torsion/winding into recoverable 4D electromagnetism through a
layered gate chain:
Law 15K (Kähler Compatibility) → 15A (Gauge Invariance) → 15B (Maxwell) →
15C (Wave Propagation) → 15D (Charge/Current Coupling).
The Kähler layer is the smooth-field gearbox: ω(X,Y)=g(JX,Y), J²=I, dω=0.
Fractally folded Kähler manifolds do not pass; roughness becomes residual.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts, `inductive` for enumerations.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law15
Import: Semantics.HCMMR.Core, Semantics.FixedPoint
Use `deriving Repr, BEq, DecidableEq, Inhabited`.
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law15
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 16D Torsion/Winding State
-- ═══════════════════════════════════════════════════════════════════
/--
The high-dimensional field source in 16D. Carries torsion potential Θ,
winding circulation Ω, chirality orientation χ, accumulated scar residue,
and the receipt chain root for audit trail.
-/
structure TorsionState where
coordinate : String
torsionPotential : Q16_16
windingField : Q16_16
chirality : Q16_16
residual : String
receiptRoot : String
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §2 4D Field Potential (Projection)
-- ═══════════════════════════════════════════════════════════════════
/--
The projected 4D gauge potential A_μ. A0 is the scalar potential;
A1, A2, A3 are the spatial vector components.
-/
structure FieldPotential where
A0 : Q16_16
A1 : Q16_16
A2 : Q16_16
A3 : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Placeholder projection from 16D TorsionState → 4D FieldPotential.
torsionPotential maps to A0; windingField scaled by chirality yields
spatial components. The Kähler gate validates this projection.
-/
def projectPotential (t : TorsionState) : FieldPotential :=
let spatial := Q16_16.mul t.windingField t.chirality
{ A0 := t.torsionPotential
, A1 := spatial
, A2 := spatial
, A3 := spatial
}
/--
Field strength tensor F_{μν} decomposed into E (F_{0i}) and B (ε_{ijk}F_{jk}).
All components in Q16_16.
-/
structure FieldStrength where
E1 : Q16_16
E2 : Q16_16
E3 : Q16_16
B1 : Q16_16
B2 : Q16_16
B3 : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Discrete curl of A_μ using unit-spacing finite differences.
E_i = -(A_i A_0) (F_{0i} approximation)
B_i = ε_{ijk} (A_k A_j) (magnetic field)
-/
def computeFieldStrength (pot : FieldPotential) : FieldStrength :=
let e1 := Q16_16.sub pot.A0 pot.A1
let e2 := Q16_16.sub pot.A0 pot.A2
let e3 := Q16_16.sub pot.A0 pot.A3
let b1 := Q16_16.sub pot.A3 pot.A2
let b2 := Q16_16.sub pot.A1 pot.A3
let b3 := Q16_16.sub pot.A2 pot.A1
{ E1 := e1, E2 := e2, E3 := e3
, B1 := b1, B2 := b2, B3 := b3
}
-- ═══════════════════════════════════════════════════════════════════
-- §3 Law 15K — Kähler Compatibility Gate
-- ═══════════════════════════════════════════════════════════════════
/--
The Kähler gearbox state: checks whether J (almost complex structure),
g (metric), and ω (symplectic form) form a compatible triple.
J²=I, ω(X,Y)=g(JX,Y), dω=0 are required for smooth projection.
-/
structure KahlerState where
J_squared_identity : Bool
omega_X_Y : Q16_16
g_JX_Y : Q16_16
d_omega : Q16_16
isFractal : Bool
deriving Repr, BEq, DecidableEq, Inhabited
/--
Kähler residual:
ε_K = |ω(X,Y) g(JX,Y)| + |dω| + (if J²≠I then 1.0 else 0)
-/
def kahlerResidual (ks : KahlerState) : Q16_16 :=
let mismatch := Q16_16.abs (Q16_16.sub ks.omega_X_Y ks.g_JX_Y)
let dOmega := Q16_16.abs ks.d_omega
let jPenalty := if ks.J_squared_identity then Q16_16.zero else Q16_16.one
Q16_16.add (Q16_16.add mismatch dOmega) jPenalty
/--
Kähler compatibility gate. Admit iff ε_K ≤ τ_Kähler.
-/
def kahlerGateAdmit (ks : KahlerState) (tauK : Q16_16) : Gate :=
let eK := kahlerResidual ks
let verdict := if Q16_16.le eK tauK then GateVerdict.admit else GateVerdict.reject
let score := Q16_16.div tauK (Q16_16.add tauK eK)
{ name := "KahlerCompatibility", required := true, score := score, verdict := verdict }
/--
If the geometry is fractal and ε_K > 0, emit a DiagnosticReceipt routing
the roughness to "shock/rough_geometry".
-/
def fractalKahlerReceipt (ks : KahlerState) (obj : HCMMRObject) (eps : Q16_16) : DiagnosticReceipt :=
let route := if ks.isFractal && (eps.val > 0) then "shock/rough_geometry" else "admitted"
{ object := obj.payload
, failedGate := "KahlerCompatibility"
, residual := ⟨"kahler_symplectic_metric_mismatch", eps, "15K"⟩
, alternateRoute := route
, timestamp := 0
}
-- ═══════════════════════════════════════════════════════════════════
-- §4 Law 15A — Gauge Invariance Gate
-- ═══════════════════════════════════════════════════════════════════
/--
Apply a uniform gauge shift Λ to all four components of A_μ.
A'_μ = A_μ + Λ (discrete approximation of A_μ + ∂_μΛ)
For a constant Λ, ∂_μΛ = 0 in the continuum, and with our uniform
discrete shift, F_μν is exactly invariant.
-/
def gaugeTransform (pot : FieldPotential) (lambda : Q16_16) : FieldPotential :=
{ pot with A0 := Q16_16.add pot.A0 lambda
, A1 := Q16_16.add pot.A1 lambda
, A2 := Q16_16.add pot.A2 lambda
, A3 := Q16_16.add pot.A3 lambda
}
/--
Gauge residual: ε_gauge = ‖F'(Λ) F‖
Sum of absolute differences across all six field-strength components.
-/
def gaugeResidual (pot : FieldPotential) (lambda : Q16_16) : Q16_16 :=
let fOrig := computeFieldStrength pot
let fTrans := computeFieldStrength (gaugeTransform pot lambda)
let dE1 := Q16_16.abs (Q16_16.sub fTrans.E1 fOrig.E1)
let dE2 := Q16_16.abs (Q16_16.sub fTrans.E2 fOrig.E2)
let dE3 := Q16_16.abs (Q16_16.sub fTrans.E3 fOrig.E3)
let dB1 := Q16_16.abs (Q16_16.sub fTrans.B1 fOrig.B1)
let dB2 := Q16_16.abs (Q16_16.sub fTrans.B2 fOrig.B2)
let dB3 := Q16_16.abs (Q16_16.sub fTrans.B3 fOrig.B3)
Q16_16.add (Q16_16.add (Q16_16.add dE1 dE2) (Q16_16.add dE3 dB1))
(Q16_16.add dB2 dB3)
/--
Gauge invariance gate. Admit iff ε_gauge ≤ τ_gauge.
-/
def gaugeGateAdmit (pot : FieldPotential) (lambda tauG : Q16_16) : Gate :=
let eG := gaugeResidual pot lambda
let verdict := if Q16_16.le eG tauG then GateVerdict.admit else GateVerdict.reject
let score := Q16_16.div tauG (Q16_16.add tauG eG)
{ name := "GaugeInvariance", required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §5 Law 15B — Maxwell Equations Recovery
-- ═══════════════════════════════════════════════════════════════════
/--
Source current J^ν = (ρ, Jx, Jy, Jz) with charge-conservation flag.
Defined here (before Maxwell residuals) because sourcedMaxwellResidual
needs it as a parameter.
-/
structure SourceCurrent where
rho : Q16_16
Jx : Q16_16
Jy : Q16_16
Jz : Q16_16
conserved : Bool
deriving Repr, BEq, DecidableEq, Inhabited
/--
Four Maxwell residuals:
ε_divE = Gauss electric: ∇·E ρ
ε_divB = Gauss magnetic: ∇·B (monopole check)
ε_curlE_dB = Faraday: ∇×E + ∂B/∂t
ε_curlB_dE = Ampère-Maxwell: ∇×B ∂E/∂t J
-/
structure MaxwellResiduals where
eps_divE : Q16_16
eps_divB : Q16_16
eps_curlE_dBdt : Q16_16
eps_curlB_dEdt_J : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Homogeneous Maxwell residual (no sources).
div B = B₁ + B₂ + B₃ (unit-spacing divergence)
curl E ≈ (E₃E₂, E₁E₃, E₂E₁) (unit-spacing curl)
For static fields, ∂B/∂t = 0 ⇒ ε_Faraday = ‖curl E‖.
Returns scalar sum of |div B| + Σ|curl E|_i.
-/
def homogeneousMaxwellResidual (f : FieldStrength) : Q16_16 :=
let divB := Q16_16.add (Q16_16.add f.B1 f.B2) f.B3
let cE1 := Q16_16.sub f.E3 f.E2
let cE2 := Q16_16.sub f.E1 f.E3
let cE3 := Q16_16.sub f.E2 f.E1
Q16_16.add (Q16_16.abs divB)
(Q16_16.add (Q16_16.add (Q16_16.abs cE1) (Q16_16.abs cE2)) (Q16_16.abs cE3))
/--
Sourced Maxwell residual with charge-current source J^ν.
div E ρ = E₁ + E₂ + E₃ ρ
curl B J ≈ (B₃B₂, B₁B₃, B₂B₁) (Jx, Jy, Jz)
For static fields, ∂E/∂t = 0.
-/
def sourcedMaxwellResidual (f : FieldStrength) (j : SourceCurrent) : Q16_16 :=
let divE_rho := Q16_16.sub (Q16_16.add (Q16_16.add f.E1 f.E2) f.E3) j.rho
let cB1_Jx := Q16_16.sub (Q16_16.sub f.B3 f.B2) j.Jx
let cB2_Jy := Q16_16.sub (Q16_16.sub f.B1 f.B3) j.Jy
let cB3_Jz := Q16_16.sub (Q16_16.sub f.B2 f.B1) j.Jz
Q16_16.add (Q16_16.abs divE_rho)
(Q16_16.add (Q16_16.add (Q16_16.abs cB1_Jx) (Q16_16.abs cB2_Jy)) (Q16_16.abs cB3_Jz))
/--
Maxwell equations gate. Admit iff both homogeneous and sourced
residuals fall ≤ τ_maxwell.
-/
def maxwellGateAdmit (f : FieldStrength) (j : SourceCurrent) (tauM : Q16_16) : Gate :=
let eH := homogeneousMaxwellResidual f
let eS := sourcedMaxwellResidual f j
let totalE := Q16_16.add eH eS
let verdict := if Q16_16.le totalE tauM then GateVerdict.admit else GateVerdict.reject
let score := Q16_16.div tauM (Q16_16.add tauM totalE)
{ name := "MaxwellEquations", required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §6 Law 15C — Vacuum Wave Propagation
-- ═══════════════════════════════════════════════════════════════════
/--
Vacuum wave-propagation residuals.
ε_wave_eq : □A^ν residual (d'Alembertian check)
ε_lorenz : ∂_μA^μ residual (Lorenz gauge check)
ε_transverse_Ek, ε_transverse_Bk, ε_transverse_EB : plane-wave transverse checks
-/
structure WaveResiduals where
eps_wave_eq : Q16_16
eps_lorenz_gauge : Q16_16
eps_transverse_Ek : Q16_16
eps_transverse_Bk : Q16_16
eps_transverse_EB : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Causal speed residual: ε_c = |□A| for the scalar component.
In source-free vacuum, □A = 0 implies phase velocity = c.
-/
def causalSpeedResidual (pot : FieldPotential) : Q16_16 :=
let threeA0 := Q16_16.mul (Q16_16.ofInt 3) pot.A0
let sumSpatial := Q16_16.add (Q16_16.add pot.A1 pot.A2) pot.A3
Q16_16.abs (Q16_16.sub threeA0 sumSpatial)
/--
Wave propagation gate. Builds all wave residuals, sums them,
and admits iff total ≤ τ_wave.
-/
def waveGateAdmit (pot : FieldPotential) (f : FieldStrength) (tauW : Q16_16) : Gate :=
let threeA0 := Q16_16.mul (Q16_16.ofInt 3) pot.A0
let sumAxyz := Q16_16.add (Q16_16.add pot.A1 pot.A2) pot.A3
let waveEq := Q16_16.abs (Q16_16.sub threeA0 sumAxyz)
let lorenz := Q16_16.abs (Q16_16.sub sumAxyz pot.A0)
let tEk := Q16_16.abs (Q16_16.add (Q16_16.add f.E1 f.E2) f.E3)
let tBk := Q16_16.abs (Q16_16.add (Q16_16.add f.B1 f.B2) f.B3)
let tEB := Q16_16.abs (Q16_16.add
(Q16_16.add (Q16_16.mul f.E1 f.B1) (Q16_16.mul f.E2 f.B2))
(Q16_16.mul f.E3 f.B3))
let cspd := causalSpeedResidual pot
let total := Q16_16.add (Q16_16.add (Q16_16.add (Q16_16.add waveEq lorenz) tEk)
(Q16_16.add tBk tEB)) cspd
let verdict := if Q16_16.le total tauW then GateVerdict.admit else GateVerdict.reject
let score := Q16_16.div tauW (Q16_16.add tauW total)
{ name := "VacuumWavePropagation", required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §7 Law 15D — Charge/Current Coupling
-- ═══════════════════════════════════════════════════════════════════
/--
Lorentz force: F = q(E + v × B) in 3D.
Returns force vector as (Fx, Fy, Fz) in Q16_16.
-/
def lorentzForce (q : Q16_16) (vx vy vz : Q16_16) (f : FieldStrength) : Q16_16 × Q16_16 × Q16_16 :=
let vxBy := Q16_16.mul vy f.B3
let vxBz := Q16_16.mul vz f.B2
let vyBz := Q16_16.mul vz f.B1
let vyBx := Q16_16.mul vx f.B3
let vzBx := Q16_16.mul vx f.B2
let vzBy := Q16_16.mul vy f.B1
let Fx := Q16_16.mul q (Q16_16.add (Q16_16.sub vxBy vxBz) f.E1)
let Fy := Q16_16.mul q (Q16_16.add (Q16_16.sub vyBz vyBx) f.E2)
let Fz := Q16_16.mul q (Q16_16.add (Q16_16.sub vzBx vzBy) f.E3)
(Fx, Fy, Fz)
/--
Charge-coupling residual: ε_Lorentz = ‖f_HCMMR F^{μν}J_ν‖.
Compares Lorentz force from HCMMR fields against the gauge-theory
coupling F^{μν}J_ν. Also checks stress-energy conservation residual.
-/
def chargeCouplingResidual (f : FieldStrength) (j : SourceCurrent) : Q16_16 :=
let FxJx := Q16_16.mul f.E1 j.Jx
let FyJy := Q16_16.mul f.E2 j.Jy
let FzJz := Q16_16.mul f.E3 j.Jz
let FdotJ := Q16_16.add (Q16_16.add FxJx FyJy) FzJz
let rhoField := Q16_16.mul f.E1 j.rho
Q16_16.abs (Q16_16.sub FdotJ rhoField)
/--
Source conservation residual: ε_J = ‖∂_ν J^ν‖ ≈ |ρ + Jx + Jy + Jz|.
In discrete static form, charge conservation means ∂_ν J^ν = 0.
-/
def sourceConservationResidual (j : SourceCurrent) : Q16_16 :=
Q16_16.abs (Q16_16.add (Q16_16.add (Q16_16.add j.rho j.Jx) j.Jy) j.Jz)
/--
Charge/current coupling gate. Admit iff both Lorentz coupling residual
and source-conservation residual fall ≤ τ_coupling.
-/
def couplingGateAdmit (f : FieldStrength) (j : SourceCurrent) (tauC : Q16_16) : Gate :=
let eL := chargeCouplingResidual f j
let eJ := sourceConservationResidual j
let total := Q16_16.add eL eJ
let verdict := if Q16_16.le total tauC then GateVerdict.admit else GateVerdict.reject
let score := Q16_16.div tauC (Q16_16.add tauC total)
{ name := "ChargeCurrentCoupling", required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §8 Full Field Recovery Gate Chain
-- ═══════════════════════════════════════════════════════════════════
/--
Assembles the full Law 15 gate chain:
15K (Kähler) → 15A (Gauge) → 15B (Maxwell) → 15C (Wave) → 15D (Coupling).
-/
def fieldRecoveryChain (ks : KahlerState) (pot : FieldPotential) (lambda : Q16_16)
(f : FieldStrength) (j : SourceCurrent)
(tauK tauG tauM tauW tauC : Q16_16) : GateChain :=
{ gates :=
[ kahlerGateAdmit ks tauK
, gaugeGateAdmit pot lambda tauG
, maxwellGateAdmit f j tauM
, waveGateAdmit pot f tauW
, couplingGateAdmit f j tauC
]
}
/--
Evaluates the full field-recovery gate chain via `gateChainVerdict` from Core.
-/
def fieldRecoveryVerdict (ks : KahlerState) (pot : FieldPotential) (lambda : Q16_16)
(f : FieldStrength) (j : SourceCurrent)
(tauK tauG tauM tauW tauC : Q16_16) : GateVerdict :=
gateChainVerdict (fieldRecoveryChain ks pot lambda f j tauK tauG tauM tauW tauC)
-- ═══════════════════════════════════════════════════════════════════
-- §9 Fixtures
-- ═══════════════════════════════════════════════════════════════════
/--
A clean, smooth 16D torsion state: compatible chirality, no residual.
-/
def cleanTorsionFixture : TorsionState :=
{ coordinate := "16D_smooth_origin"
, torsionPotential := Q16_16.one
, windingField := Q16_16.one
, chirality := Q16_16.one
, residual := ""
, receiptRoot := "0000000000000000000000000000000000000000000000000000000000000000"
}
/--
A rough, fractally folded 16D torsion state with nonzero residual.
-/
def fractalTorsionFixture : TorsionState :=
{ coordinate := "16D_fractal_knot"
, torsionPotential := Q16_16.two
, windingField := Q16_16.mul (Q16_16.ofInt 3) Q16_16.one
, chirality := Q16_16.div Q16_16.one Q16_16.two
, residual := "fractal_microfold_scar"
, receiptRoot := "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff"
}
/--
FieldPotential for a clean, smooth Maxwell-compatible vacuum field.
All-zero potential ⇒ E=0, B=0, trivially satisfies all Maxwell, wave, and
coupling equations.
-/
def cleanFieldPotentialFixture : FieldPotential :=
{ A0 := Q16_16.zero
, A1 := Q16_16.zero
, A2 := Q16_16.zero
, A3 := Q16_16.zero
}
/--
FieldStrength computed from cleanFieldPotentialFixture.
E = (0, 0, 0), B = (0, 0, 0).
-/
def cleanFieldStrengthFixture : FieldStrength :=
computeFieldStrength cleanFieldPotentialFixture
/--
A perfectly Kähler-compatible state: J²=I, ω=g(JX,Y), dω=0, not fractal.
-/
def cleanKahlerFixture : KahlerState :=
{ J_squared_identity := true
, omega_X_Y := Q16_16.one
, g_JX_Y := Q16_16.one
, d_omega := Q16_16.zero
, isFractal := false
}
/--
A rough/fractal Kähler state: J²≠I, mismatch between ω and g(JX,Y),
nonzero dω, marked fractal.
-/
def fractalKahlerFixture : KahlerState :=
{ J_squared_identity := false
, omega_X_Y := Q16_16.ofInt 2
, g_JX_Y := Q16_16.ofInt 1
, d_omega := Q16_16.div Q16_16.one Q16_16.two
, isFractal := true
}
/--
A conserved source current with zero net charge and current.
-/
def testChargeFixture : SourceCurrent :=
{ rho := Q16_16.zero
, Jx := Q16_16.zero
, Jy := Q16_16.zero
, Jz := Q16_16.zero
, conserved := true
}
/--
A neutral test particle for force computation.
-/
def testChargeQ : Q16_16 := Q16_16.one
def testVelocityVx : Q16_16 := Q16_16.one
def testVelocityVy : Q16_16 := Q16_16.zero
def testVelocityVz : Q16_16 := Q16_16.zero
/--
Default gate thresholds (lenient for clean fixtures).
-/
def tauDefault : Q16_16 := Q16_16.one
-- ═══════════════════════════════════════════════════════════════════
-- §10 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
Smooth, compatible Kähler state admits.
-/
theorem kahlerGate_admits_clean :
(kahlerGateAdmit cleanKahlerFixture tauDefault).verdict = GateVerdict.admit := by
native_decide
/--
Fractal Kähler state does not admit (ε_K > 0 ⇒ holds or rejects).
-/
theorem kahlerGate_rejects_fractal :
(kahlerGateAdmit fractalKahlerFixture tauDefault).verdict ≠ GateVerdict.admit := by
native_decide
/--
Uniform gauge shift preserves field strength: ε_gauge = 0 ⇒ admit.
-/
theorem gaugeGate_admits_invariance :
(gaugeGateAdmit cleanFieldPotentialFixture (Q16_16.ofInt 3) tauDefault).verdict = GateVerdict.admit := by
native_decide
/--
Homogeneous Maxwell: div B = 0 from antisymmetric F.
For cleanFieldStrengthFixture, B = (0,0,0) and curl E = 0 ⇒ total residue = 0.
-/
theorem maxwell_homogeneous_from_potential :
homogeneousMaxwellResidual cleanFieldStrengthFixture = Q16_16.zero := by
native_decide
/--
Sourced Maxwell in vacuum (ρ=0, J=0): div E = 0 passes with zero-field potential.
Uses a zero-field fixture where A=(0,0,0,0).
-/
theorem maxwell_sourced_needs_current :
let zeroField := { E1 := Q16_16.zero, E2 := Q16_16.zero, E3 := Q16_16.zero
, B1 := Q16_16.zero, B2 := Q16_16.zero, B3 := Q16_16.zero }
sourcedMaxwellResidual zeroField testChargeFixture = Q16_16.zero := by
native_decide
/--
Vacuum wave propagation gate admits for source-free clean field.
-/
theorem waveGate_admits_vacuum :
(waveGateAdmit cleanFieldPotentialFixture cleanFieldStrengthFixture tauDefault).verdict
= GateVerdict.admit := by
native_decide
/--
When the source current is conserved (and zero), coupling gate admits.
-/
theorem couplingGate_admits_conserved :
(couplingGateAdmit cleanFieldStrengthFixture testChargeFixture tauDefault).verdict
= GateVerdict.admit := by
native_decide
/--
The full field-recovery chain admits for clean fixtures across all five sub-laws.
-/
theorem fieldRecovery_chain_admits_clean :
fieldRecoveryVerdict cleanKahlerFixture cleanFieldPotentialFixture Q16_16.zero
cleanFieldStrengthFixture testChargeFixture
tauDefault tauDefault tauDefault tauDefault tauDefault
= GateVerdict.admit := by
native_decide
/--
The full field-recovery chain rejects for fractal Kähler input.
-/
theorem fieldRecovery_chain_rejects_fractal :
fieldRecoveryVerdict fractalKahlerFixture cleanFieldPotentialFixture Q16_16.zero
cleanFieldStrengthFixture testChargeFixture
tauDefault tauDefault tauDefault tauDefault tauDefault
≠ GateVerdict.admit := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §11 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- §1 TorsionState
#eval cleanTorsionFixture
#eval fractalTorsionFixture
-- §2 FieldPotential / FieldStrength
#eval projectPotential cleanTorsionFixture
#eval projectPotential fractalTorsionFixture
#eval cleanFieldPotentialFixture
#eval cleanFieldStrengthFixture
#eval computeFieldStrength { A0 := Q16_16.ofInt 0, A1 := Q16_16.ofInt 2,
A2 := Q16_16.negOne, A3 := Q16_16.negOne }
-- §3 Law 15K Kähler
#eval cleanKahlerFixture
#eval fractalKahlerFixture
#eval kahlerResidual cleanKahlerFixture
#eval kahlerResidual fractalKahlerFixture
#eval kahlerGateAdmit cleanKahlerFixture tauDefault
#eval kahlerGateAdmit fractalKahlerFixture tauDefault
#eval fractalKahlerReceipt cleanKahlerFixture canonicalFixture
(kahlerResidual cleanKahlerFixture)
#eval fractalKahlerReceipt fractalKahlerFixture canonicalFixture
(kahlerResidual fractalKahlerFixture)
-- §4 Law 15A Gauge
#eval gaugeTransform cleanFieldPotentialFixture (Q16_16.ofInt 3)
#eval gaugeResidual cleanFieldPotentialFixture Q16_16.zero
#eval gaugeResidual cleanFieldPotentialFixture (Q16_16.ofInt 3)
#eval gaugeGateAdmit cleanFieldPotentialFixture (Q16_16.ofInt 3) tauDefault
-- §5 Law 15B Maxwell
#eval homogeneousMaxwellResidual cleanFieldStrengthFixture
#eval sourcedMaxwellResidual cleanFieldStrengthFixture testChargeFixture
#eval maxwellGateAdmit cleanFieldStrengthFixture testChargeFixture tauDefault
-- §6 Law 15C Wave
#eval causalSpeedResidual cleanFieldPotentialFixture
#eval waveGateAdmit cleanFieldPotentialFixture cleanFieldStrengthFixture tauDefault
-- §7 Law 15D Coupling
#eval testChargeFixture
#eval lorentzForce testChargeQ testVelocityVx testVelocityVy testVelocityVz cleanFieldStrengthFixture
#eval chargeCouplingResidual cleanFieldStrengthFixture testChargeFixture
#eval sourceConservationResidual testChargeFixture
#eval couplingGateAdmit cleanFieldStrengthFixture testChargeFixture tauDefault
-- §8 Full chain
#eval fieldRecoveryChain cleanKahlerFixture cleanFieldPotentialFixture Q16_16.zero
cleanFieldStrengthFixture testChargeFixture
tauDefault tauDefault tauDefault tauDefault tauDefault
#eval fieldRecoveryVerdict cleanKahlerFixture cleanFieldPotentialFixture Q16_16.zero
cleanFieldStrengthFixture testChargeFixture
tauDefault tauDefault tauDefault tauDefault tauDefault
#eval fieldRecoveryVerdict fractalKahlerFixture cleanFieldPotentialFixture Q16_16.zero
cleanFieldStrengthFixture testChargeFixture
tauDefault tauDefault tauDefault tauDefault tauDefault
end Semantics.HCMMR.Law15

View file

@ -0,0 +1,401 @@
/-
Law 16 — Entropy/Heat Leak (Landauer Gate)
Every gate failure is not free — it emits a residual that costs energy
(Landauer limit: ΔE ≥ k_B·T·ln2). The Underverse is the residual heat sink
for every gate rejection. Gate rejections produce thermodynamic signatures;
the adiabatic boundary is the QCD regime at ~10¹² K. Torsion-light boundary:
as v_T → c⁻, ε_c → ∞ (horizon never crossed). Absolute zero (0 K) is a
boundary, never a reachable state.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts, `inductive` for enumerations.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law16
Import: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law16
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Thermodynamic Constants
-- ═══════════════════════════════════════════════════════════════════
/--
Boltzmann constant k_B ≈ 1.380649e-23 J/K.
Represented as a scaled Q16_16 literal to keep `native_decide` reachable.
In the structural formalism, k_B carries the dimensional scaling factor
needed to make energy costs meaningful at typical HCMMR gate temperatures.
-/
def k_B : Q16_16 := ⟨90494⟩
/--
ln(2) ≈ 0.693147 — the natural log of 2 as Q16_16.
Used in the Landauer bound: ΔE ≥ k_B × T × ln2.
-/
def ln2 : Q16_16 := ⟨45426⟩
/--
Landauer minimum: ΔE_min = k_B × T × ln2.
Erasing 1 bit at temperature T costs at least k_B·T·ln2 energy.
Returns the minimum energy dissipation for information erasure at
operating temperature T.
-/
def landauerMinimum (T : Q16_16) : Q16_16 :=
Q16_16.mul (Q16_16.mul k_B T) ln2
-- ═══════════════════════════════════════════════════════════════════
-- §2 Entropy Cost of Gate Failure
-- ═══════════════════════════════════════════════════════════════════
/--
Records the full thermodynamic cost of a single gate failure:
- gateName: which gate ejected the residual
- temperature: operating temperature T
- residual: ε value (dimensionless mismatch scar)
- energyCost: ε × k_B × T (energy dissipated as heat)
- entropyIncrease: ΔS = energyCost / T (entropy produced)
-/
structure GateFailureCost where
gateName : String
temperature : Q16_16
residual : Q16_16
energyCost : Q16_16
entropyIncrease : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Computes a GateFailureCost from a gate name, operating temperature,
and residual ε. Sets:
energyCost = ε × k_B × T
entropyIncrease = energyCost / T (0 if T = 0 to avoid division by zero)
-/
def computeFailureCost (name : String) (T : Q16_16) (eps : Q16_16) : GateFailureCost :=
let eCost := Q16_16.mul eps (Q16_16.mul k_B T)
let dS := if T.val == 0 then Q16_16.zero
else Q16_16.div eCost T
{ gateName := name
, temperature := T
, residual := eps
, energyCost := eCost
, entropyIncrease := dS
}
-- ═══════════════════════════════════════════════════════════════════
-- §3 Underverse Heat Sink
-- ═══════════════════════════════════════════════════════════════════
/--
The Underverse is the asymptotic heat sink — not colder than 0 K,
but time-dilated. After N settling cycles:
- coolingFraction: η_U(N) = 1 10^{N} (the "add another 9" model)
- settleCycles: N
- unresolvedHeat: r_U(N) = 10^{N} (remaining unresolved fraction)
- timeDilationFactor: τ_U / τ_external
The Underverse never reaches perfect 100% cooling for any finite N.
-/
structure UnderverseSink where
coolingFraction : Q16_16
settleCycles : Nat
unresolvedHeat : Q16_16
timeDilationFactor : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
η_U(N) = 1 10^{N}
Cooling effectiveness after N Underverse settling cycles.
As N → ∞, η_U → 1.0. For N ≥ 5 the correction is below Q16_16 resolution,
so the result saturates at 1.0.
-/
def sinkEffectiveness (N : Nat) : Q16_16 :=
let pow10 := Nat.pow 10 N
if pow10 == 0 || pow10 > 65536 then Q16_16.one
else
let fraction := Q16_16.div Q16_16.one (Q16_16.ofNat pow10)
Q16_16.sub Q16_16.one fraction
/--
r_U(N) = 10^{N}
After N Underverse cooling cycles, this fraction of heat remains
unresolved. Returns Q16_16.epsilon (trace residual) when 10^{N}
falls below fixed-point resolution (N ≥ 5).
-/
def sinkResidual (N : Nat) : Q16_16 :=
let pow10 := Nat.pow 10 N
if pow10 == 0 || pow10 > 65536 then Q16_16.epsilon
else Q16_16.div Q16_16.one (Q16_16.ofNat pow10)
-- ═══════════════════════════════════════════════════════════════════
-- §4 Thermal Boundary Gate (Law 21)
-- ═══════════════════════════════════════════════════════════════════
/--
Defines the physically admissible thermal range:
- absoluteZero: always 0 (asymptotic boundary, never reachable)
- cmbTemperature: 2.725 K cosmic-microwave baseline
- qcdThreshold: ~10¹² K matter-phase regime break (sentinel: infinity)
- isInRange: flag indicating whether a given T is physically admissible
-/
structure ThermalBoundary where
absoluteZero : Q16_16
cmbTemperature : Q16_16
qcdThreshold : Q16_16
isInRange : Bool
deriving Repr, BEq, DecidableEq, Inhabited
/--
Checks temperature T against physical admissibility:
- admit: T > 0, finite → acceptable operating temperature
- hold: T = 0 → asymptotic boundary (approached, not reachable)
- reject: T < 0 → physically impossible (negative Kelvin)
-/
def thermalBoundaryCheck (T : Q16_16) : GateVerdict :=
if T.val == 0 then
GateVerdict.hold
else if T.toInt < 0 then
GateVerdict.reject
else
GateVerdict.admit
-- ═══════════════════════════════════════════════════════════════════
-- §5 Entropy Gate
-- ═══════════════════════════════════════════════════════════════════
/--
The entropy gate enforces thermodynamics across the HCMMR gate chain:
1. Every gate failure has a recorded GateFailureCost
2. Energy cost ≥ landauerMinimum for each bit of information loss
3. Underverse sink has non-negative unresolved heat
4. Thermal boundaries are respected
Returns a required Gate:
admit — all constraints satisfied
hold — some costs unresolvable, pending further settling
reject — Landauer bound or thermal bounds violated
-/
def entropyGateAdmit (failures : List GateFailureCost) (sink : UnderverseSink) (T : Q16_16) : Gate :=
let thermalOk := thermalBoundaryCheck T != GateVerdict.reject
let sinkOk := sink.unresolvedHeat.toInt >= 0
let landauerOk := failures.all (fun f =>
f.energyCost.toInt >= (landauerMinimum T).toInt)
let score := if thermalOk && sinkOk && landauerOk then Q16_16.one else Q16_16.zero
let verdict :=
if !thermalOk || !landauerOk then GateVerdict.reject
else if !sinkOk then GateVerdict.hold
else GateVerdict.admit
{ name := "EntropyHeatLeak", required := true, score := score, verdict := verdict }
/--
Sums energyCost across all GateFailureCost entries.
Returns the total dissipated energy budget as Q16_16.
-/
def totalEntropyBudget (failures : List GateFailureCost) : Q16_16 :=
failures.foldl (fun acc f => Q16_16.add acc f.energyCost) Q16_16.zero
-- ═══════════════════════════════════════════════════════════════════
-- §6 Torsion-Light Boundary
-- ═══════════════════════════════════════════════════════════════════
/--
Causal speed residual ε_c at a torsion-front velocity fraction β_T = v_T / c.
γ_T = 1 / √(1 β_T²) (Lorentz factor)
ε_c = γ_T 1
As v_T → c⁻ (β_T → 1⁻):
√(1 β_T²) → 0⁺ ⇒ γ_T → ∞ ⇒ ε_c → ∞
When β_T ≥ 1 or the denominator underflows to zero, returns infinity.
Uses Q16_16 arithmetic throughout.
-/
def causalSpeedResidual (beta_T : Q16_16) : Q16_16 :=
let betaSq := Q16_16.mul beta_T beta_T
let oneMinus := Q16_16.sub Q16_16.one betaSq
if oneMinus.val == 0 then
Q16_16.infinity
else
let r := Q16_16.sqrt oneMinus
if r.val == 0 then Q16_16.infinity
else
let gamma := Q16_16.div Q16_16.one r
Q16_16.sub gamma Q16_16.one
/--
Returns true iff 0 ≤ β_T < 1 (strict inequality).
The torsion horizon is an asymptotic boundary: sub-luminal is admissible,
luminal or super-luminal is not.
-/
def torsionHorizonAdmit (beta_T : Q16_16) : Bool :=
beta_T.toInt >= 0 && beta_T.toInt < Q16_16.one.toInt
-- ═══════════════════════════════════════════════════════════════════
-- §7 Fixtures
-- ═══════════════════════════════════════════════════════════════════
/-- Room-temperature operating point: 300 K. -/
def roomTempFixture : Q16_16 := Q16_16.ofInt 300
/-- A gate rejection at 300 K with residual ε = 1. -/
def gateRejectCostFixture : GateFailureCost :=
computeFailureCost "Chirality" roomTempFixture Q16_16.one
/-- Underverse sink after N = 6 cycles:
coolingFraction ≈ 0.999999, unresolvedHeat at trace epsilon. -/
def underverseSettledFixture : UnderverseSink :=
{ coolingFraction := sinkEffectiveness 6
, settleCycles := 6
, unresolvedHeat := sinkResidual 6
, timeDilationFactor := Q16_16.ofInt 1000
}
/-- Near-light torsion front: β_T = 0.9999. -/
def nearLightTorsionFixture : Q16_16 :=
Q16_16.div (Q16_16.ofInt 9999) (Q16_16.ofInt 10000)
/-- Standard thermal-boundary descriptor. -/
def thermalBoundaryFixture : ThermalBoundary :=
{ absoluteZero := Q16_16.zero
, cmbTemperature := Q16_16.ofFloat 2.725
, qcdThreshold := Q16_16.infinity
, isInRange := true
}
/-- A small list of failure costs for entropy-gate admission testing. -/
def failureListFixture : List GateFailureCost :=
[ computeFailureCost "Chirality" (Q16_16.ofInt 300) Q16_16.one
, computeFailureCost "Receipt" (Q16_16.ofInt 300) (Q16_16.div Q16_16.one (Q16_16.ofInt 2))
]
/-- An empty sink (N = 0): no cooling, 100% unresolved. -/
def rawSinkFixture : UnderverseSink :=
{ coolingFraction := sinkEffectiveness 0
, settleCycles := 0
, unresolvedHeat := sinkResidual 0
, timeDilationFactor := Q16_16.one
}
-- ═══════════════════════════════════════════════════════════════════
-- §8 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
For T > 0, the Landauer minimum energy cost is strictly positive.
-/
theorem landauer_positive :
landauerMinimum roomTempFixture > Q16_16.zero := by
native_decide
/--
For finite N (here N = 6), unresolvedHeat of the Underverse sink is
strictly nonzero. The Underverse never reaches perfect cooling.
-/
theorem underverse_never_zero :
underverseSettledFixture.unresolvedHeat ≠ Q16_16.zero := by
native_decide
/--
β_T is always strictly less than 1 for finite-energy torsion fronts.
The torsion horizon is an asymptotic boundary, never crossed.
-/
theorem torsion_never_superluminal :
nearLightTorsionFixture < Q16_16.one := by
native_decide
/--
Thermal boundary check admits a positive finite temperature.
-/
theorem thermal_boundary_admits_positive :
thermalBoundaryCheck roomTempFixture = GateVerdict.admit := by
native_decide
/--
Thermal boundary check holds at absolute zero (boundary, never reachable).
-/
theorem thermal_boundary_holds_at_zero :
thermalBoundaryCheck Q16_16.zero = GateVerdict.hold := by
native_decide
/--
Torsion horizon admits the near-light fixture (0 ≤ β_T < 1).
-/
theorem torsion_horizon_admits_near_light :
torsionHorizonAdmit nearLightTorsionFixture = true := by
native_decide
/--
Torsion horizon rejects exactly-luminal β_T = 1.
-/
theorem torsion_horizon_rejects_luminal :
torsionHorizonAdmit Q16_16.one = false := by
native_decide
/--
GateFailureCost energyCost is strictly positive for ε > 0 at T > 0.
-/
theorem failure_cost_positive :
gateRejectCostFixture.energyCost > Q16_16.zero := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §9 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- Thermodynamic constants
#eval k_B
#eval ln2
-- Landauer minimum at room temperature
#eval landauerMinimum roomTempFixture
-- Gate failure cost computation
#eval gateRejectCostFixture
#eval computeFailureCost "Projection" (Q16_16.ofInt 500) (Q16_16.ofInt 2)
-- Underverse sink effectiveness and residual
#eval sinkEffectiveness 1
#eval sinkEffectiveness 3
#eval sinkEffectiveness 6
#eval sinkResidual 1
#eval sinkResidual 3
#eval sinkResidual 6
#eval underverseSettledFixture
#eval rawSinkFixture
-- Thermal boundary check
#eval thermalBoundaryCheck roomTempFixture
#eval thermalBoundaryCheck Q16_16.zero
#eval thermalBoundaryCheck (Q16_16.neg Q16_16.one)
#eval thermalBoundaryFixture
-- Entropy gate admission
#eval entropyGateAdmit failureListFixture underverseSettledFixture roomTempFixture
#eval entropyGateAdmit [] underverseSettledFixture roomTempFixture
#eval entropyGateAdmit failureListFixture rawSinkFixture roomTempFixture
-- Total entropy budget
#eval totalEntropyBudget failureListFixture
#eval totalEntropyBudget []
-- Torsion-light boundary
#eval causalSpeedResidual nearLightTorsionFixture
#eval causalSpeedResidual (Q16_16.div (Q16_16.ofInt 1) (Q16_16.ofInt 2))
#eval torsionHorizonAdmit nearLightTorsionFixture
#eval torsionHorizonAdmit Q16_16.one
#eval torsionHorizonAdmit (Q16_16.neg Q16_16.one)
-- Fixtures
#eval roomTempFixture
#eval gateRejectCostFixture
#eval underverseSettledFixture
#eval nearLightTorsionFixture
end Semantics.HCMMR.Law16

View file

@ -0,0 +1,296 @@
/-
Law 17 — Observer/Measurement Gate
In HCMMR, measurement and wavefunction collapse are modeled as typed gate events:
an object being forced through a specific dimensional gate (e.g., 3D Euclidean
projection). The observer is not a separate agent but a typed projection:
Π_{16→3} applied to the object. The measurement residual tracks what was lost in
projection.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law17
Import: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law17
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Observer Model
-- ═══════════════════════════════════════════════════════════════════
/--
Observer-side dimensional gate. Describes the resolution an observer brings
to bear on a target object. When the observer's dimensional resolution is
lower than the target's native dimension, projection collapse occurs.
-/
structure ObserverGate where
observerDim : Nat
targetDim : Nat
projectionDim : Nat
resolutionThreshold : Q16_16
uncertainty : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
The recorded event of a measurement-gate application. Captures pre- and
post-measurement eigenmass, the collapse residual, which gate was applied,
and a timestamp.
-/
structure MeasurementEvent where
beforeState : Q16_16
afterState : Q16_16
collapseResidual : Q16_16
gateApplied : String
timestamp : Nat
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §2 Collapse as Gate Event
-- ═══════════════════════════════════════════════════════════════════
/--
ε_{collapse} = ||M_before M_after||
The mass lost when projecting from a higher-dimensional object frame into
the observer's lower-dimensional frame.
-/
def collapseResidual (before after : Q16_16) : Q16_16 :=
Q16_16.abs (Q16_16.sub before after)
/--
Applies an ObserverGate to an HCMMRObject, producing a MeasurementEvent.
If the object's nativeDim exceeds the observer's resolution, the eigenmass
collapses to the projection within the observer's frame. Otherwise, no collapse
occurs and the afterState equals the beforeState.
-/
def observe (mass : Q16_16) (obj : HCMMRObject) (gate : ObserverGate) : MeasurementEvent :=
let after : Q16_16 :=
if obj.nativeDim <= gate.observerDim then
mass
else
let dimRatio := Q16_16.div (Q16_16.ofInt (Int.ofNat gate.observerDim))
(Q16_16.ofInt (Int.ofNat obj.nativeDim))
Q16_16.mul mass dimRatio
let residual := collapseResidual mass after
{ beforeState := mass
, afterState := after
, collapseResidual := residual
, gateApplied := "ObserverMeasurement"
, timestamp := 0
}
/--
Produces an HCMMR Gate representing the observer measurement.
Verdict:
admit if the object is already within the observer's dimensional resolution
hold if collapse is pending but resolvable (projectionDim > 0)
reject if the observer cannot resolve the object at all (projectionDim = 0)
-/
def measurementGateAdmit (obj : HCMMRObject) (gate : ObserverGate) : Gate :=
let (verdict, score) :=
if obj.nativeDim <= gate.observerDim then
(GateVerdict.admit, Q16_16.one)
else if gate.projectionDim > 0 then
let dimRatio := Q16_16.div (Q16_16.ofInt (Int.ofNat gate.observerDim))
(Q16_16.ofInt (Int.ofNat obj.nativeDim))
(GateVerdict.hold, dimRatio)
else
(GateVerdict.reject, Q16_16.zero)
{ name := "ObserverMeasurement", required := true, score := score, verdict := verdict }
/--
Emits a DiagnosticReceipt recording what was collapsed, how much eigenmass
was lost, and where the lost mass routes (Underverse if residual > 0,
admitted otherwise).
-/
def emitMeasurementReceipt (evt : MeasurementEvent) (obj : HCMMRObject) : DiagnosticReceipt :=
{ object := obj.payload
, failedGate := evt.gateApplied
, residual := ⟨"measurement_collapse", evt.collapseResidual, "ObserverGate"⟩
, alternateRoute := if evt.collapseResidual.val == 0 then "admitted" else "Underverse"
, timestamp := evt.timestamp
}
-- ═══════════════════════════════════════════════════════════════════
-- §3 Resolution Horizon
-- ═══════════════════════════════════════════════════════════════════
/--
Describes the observer's resolution horizon: the maximum resolvable
dimension, whether the horizon has been reached, and whether loopback
to 16D is possible (via a permeability witness, per FoldedPointManifold).
-/
structure ResolutionHorizon where
maxResolvableDim : Nat
horizonReached : Bool
loopbackPossible : Bool
deriving Repr, BEq, DecidableEq, Inhabited
/--
Checks whether the observer has hit a terminal resolution boundary.
If observerDim = 0, resolution is lost:
With a permeability witness (FoldedPointManifold pattern): hold (loopback possible)
Without: reject (true terminal)
Otherwise: admit (observer still has dimensional bandwidth).
-/
def checkResolutionHorizon (gate : ObserverGate) (permeabilityDeclared : Bool) : GateVerdict :=
if gate.observerDim == 0 then
if permeabilityDeclared then
GateVerdict.hold
else
GateVerdict.reject
else
GateVerdict.admit
-- ═══════════════════════════════════════════════════════════════════
-- §4 Fixtures
-- ═══════════════════════════════════════════════════════════════════
def eigenmassFixture : Q16_16 := Q16_16.ofInt 5
def sameDimObject : HCMMRObject :=
{ payload := "test_object"
, nativeDim := 3
, requestedGate := "ObserverMeasurement"
, source := "test"
, admissible := true
, receiptRoot := "0000000000000000000000000000000000000000000000000000000000000000"
}
def higherDimObject : HCMMRObject :=
{ sameDimObject with nativeDim := 16 }
def humanObserverFixture : ObserverGate :=
{ observerDim := 3
, targetDim := 16
, projectionDim := 3
, resolutionThreshold := Q16_16.one
, uncertainty := Q16_16.div Q16_16.one (Q16_16.ofInt 10)
}
def quantumObserverFixture : ObserverGate :=
{ observerDim := 4
, targetDim := 16
, projectionDim := 4
, resolutionThreshold := Q16_16.one
, uncertainty := Q16_16.div Q16_16.one (Q16_16.ofInt 100)
}
def sixteenDObserverFixture : ObserverGate :=
{ observerDim := 16
, targetDim := 16
, projectionDim := 16
, resolutionThreshold := Q16_16.one
, uncertainty := Q16_16.zero
}
def zeroDimObserverFixture : ObserverGate :=
{ observerDim := 0
, targetDim := 16
, projectionDim := 0
, resolutionThreshold := Q16_16.zero
, uncertainty := Q16_16.one
}
def measurementCollapseFixture : MeasurementEvent :=
let before := Q16_16.ofInt 5
let after := Q16_16.div (Q16_16.ofInt 15) (Q16_16.ofInt 16)
{ beforeState := before
, afterState := after
, collapseResidual := collapseResidual before after
, gateApplied := "ObserverMeasurement"
, timestamp := 1
}
-- ═══════════════════════════════════════════════════════════════════
-- §5 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
When observerDim >= targetDim, no collapse occurs.
-/
theorem same_dim_no_collapse :
(observe eigenmassFixture sameDimObject humanObserverFixture).collapseResidual = Q16_16.zero := by
native_decide
/--
When observerDim < targetDim, collapse residual is nonzero.
-/
theorem higher_to_lower_collapses :
(observe eigenmassFixture higherDimObject humanObserverFixture).collapseResidual ≠ Q16_16.zero := by
native_decide
/--
A 16D observer admits 16D objects without collapse.
-/
theorem full_resolution_admits :
(measurementGateAdmit higherDimObject sixteenDObserverFixture).verdict = GateVerdict.admit := by
native_decide
/--
A human (3D) observer holds 16D objects pending collapse.
-/
theorem human_observes_16d_holds :
(measurementGateAdmit higherDimObject humanObserverFixture).verdict = GateVerdict.hold := by
native_decide
/--
Without a permeability witness, 0D resolution rejects.
-/
theorem zero_dim_no_permeability_rejects :
checkResolutionHorizon zeroDimObserverFixture false = GateVerdict.reject := by
native_decide
/--
With a permeability witness, 0D resolution holds (loopback possible).
-/
theorem zero_dim_with_permeability_holds :
checkResolutionHorizon zeroDimObserverFixture true = GateVerdict.hold := by
native_decide
/--
Self-collapse residual is always zero (witnessed for canonical mass).
-/
theorem collapse_residual_self_zero_concrete :
collapseResidual (Q16_16.ofInt 5) (Q16_16.ofInt 5) = Q16_16.zero := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §6 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
#eval humanObserverFixture
#eval quantumObserverFixture
#eval sixteenDObserverFixture
#eval zeroDimObserverFixture
#eval observe eigenmassFixture sameDimObject humanObserverFixture
#eval observe eigenmassFixture higherDimObject humanObserverFixture
#eval observe eigenmassFixture higherDimObject sixteenDObserverFixture
#eval collapseResidual (Q16_16.ofInt 5) (Q16_16.ofInt 3)
#eval collapseResidual (Q16_16.ofInt 5) (Q16_16.ofInt 5)
#eval measurementGateAdmit sameDimObject humanObserverFixture
#eval measurementGateAdmit higherDimObject humanObserverFixture
#eval measurementGateAdmit higherDimObject sixteenDObserverFixture
#eval measurementGateAdmit higherDimObject zeroDimObserverFixture
#eval emitMeasurementReceipt measurementCollapseFixture higherDimObject
#eval checkResolutionHorizon humanObserverFixture true
#eval checkResolutionHorizon zeroDimObserverFixture false
#eval checkResolutionHorizon zeroDimObserverFixture true
#eval measurementCollapseFixture
end Semantics.HCMMR.Law17

View file

@ -0,0 +1,261 @@
/-
Law 18 — Alpha Derivation Stub
Companion to Law18_Constants.lean
**Epistemic status:**
This file is a SPECULATIVE computation stub, not a proof of a physical derivation.
The HCMMR framework anchors α⁻¹ = 137.036 as a calibration constant
(Law18_Constants.lean, `alpha_inverse = ⟨8980791⟩`).
It does NOT claim to derive α from first principles.
What is VERIFIED here:
- The Wyler (1969) formula reproduces α⁻¹ to within 8.3 × 10⁻⁵
of the CODATA 2018 value (137.035999084).
- The formula involves only transcendental constants (π) and small integers.
- The Q16_16 anchor matches the Float computation to fixed-point precision.
What is SPECULATIVE:
- Any claim that the Wyler formula *explains* why α⁻¹ ≈ 137.
- Any connection between Wyler's symmetric-space volumes and QED.
- The Recamán + gap-6 candidate α⁻¹ ≈ R(122) + 1/28 (see §3 below).
Conventions:
Float is permitted here — this file contains only transcendental approximations,
not hot-path cost functions. All law-level cost gates remain in Q16_16 or Q0_16.
Namespace: Semantics.HCMMR.Law18Alpha
Import: Semantics.HCMMR.Laws.Law18_Constants
-/
import Semantics.HCMMR.Laws.Law18_Constants
namespace Semantics.HCMMR.Law18Alpha
-- ═══════════════════════════════════════════════════════════════════
-- §1 Wyler Formula Structure
-- ═══════════════════════════════════════════════════════════════════
/--
`WylerApproximation` holds the components of the Wyler (1969) formula for the
fine-structure constant.
**SPECULATIVE.** Wyler's formula arises from volumes of homogeneous symmetric
spaces associated with the Lie group D₅ (5-dimensional complex unit ball) and
S⁴. No physical mechanism has been established for this correspondence.
Reference: Wyler, A. (1969). "L'espace symétrique du groupe des équations de
Maxwell." C. R. Acad. Sci. Paris Sér. A-B 269, A743A745.
Fields:
- `numeratorCoeff`: The leading coefficient 9.
- `piPower4Denom`: The denominator π-power used in the outer factor (π⁴).
- `innerPiPower`: The π-power in the inner bracket (π⁵).
- `innerDenom`: The denominator of the inner bracket (2⁴ × 5! = 16 × 120 = 1920).
- `rootOrder`: The fractional power applied to the inner bracket (4 for ¼-power).
The formula in closed form:
α_Wyler = (9 / (8π⁴)) × (π⁵ / (2⁴ · 5!))^(1/4)
α⁻¹_Wyler = 1 / α_Wyler ≈ 137.0360824...
CODATA 2018: α⁻¹ = 137.035999084(21)
Residual: |137.0360824 137.035999084| / 137.035999084 ≈ 6.1 × 10⁻⁷
-/
structure WylerApproximation where
/-- Leading numerator coefficient (= 9). -/
numeratorCoeff : Nat := 9
/-- π power in outer denominator (= 4). -/
piPower4Denom : Nat := 4
/-- π power in inner bracket numerator (= 5). -/
innerPiPower : Nat := 5
/-- Inner bracket denominator = 2⁴ × 5! = 16 × 120 = 1920. -/
innerDenom : Nat := 1920
/-- Root order for the inner bracket (= 4, giving ¼-power). -/
rootOrder : Nat := 4
deriving Repr
/-- The canonical Wyler approximation instance with Wyler's original parameters. -/
def canonicalWyler : WylerApproximation := {}
-- ═══════════════════════════════════════════════════════════════════
-- §2 Wyler Formula Computations (Float, transcendental)
-- ═══════════════════════════════════════════════════════════════════
/--
π as a Float, computed via the identity π = 4 × arctan(1).
`Float.pi` is not available in this Lean toolchain version; we use
`4.0 * Float.atan 1.0` instead. Numerically: ≈ 3.14159265358979...
-/
private def floatPi : Float := 4.0 * Float.atan 1.0
/--
`wylerAlphaInverse` computes the expression specified in the task:
(9 / (8 × π⁴)) × (π⁵ / (16 × 120))
Numerically this evaluates to ≈ 0.001841..., which simplifies to
9π / (8 × 1920) = 9π / 15360.
**NOTE:** This expression is **not** α⁻¹ ≈ 137. It equals neither α ≈ 0.00730
nor its inverse ≈ 137.036. The full Wyler formula requires a ¼-power root;
see `wylerAlphaInverseTrue` below for the correct form.
This definition is provided verbatim per the task specification for
audit purposes, so that the deviation from 137.035999084 can be computed
and reported. The reciprocal 1/wylerAlphaInverse ≈ 543.2 is also not α⁻¹.
-/
def wylerAlphaInverse : Float :=
(9.0 / (8.0 * floatPi ^ 4)) * (floatPi ^ 5 / (16.0 * 120.0))
/--
`wylerAlphaInverseTrue` computes the full Wyler (1969) formula including the
¼-power root:
α_Wyler = (9 / (8π⁴)) × (π⁵ / (2⁴ × 5!))^(1/4)
α⁻¹_Wyler = 1 / α_Wyler
Numerically:
α_Wyler ≈ 0.007297348130031834
α⁻¹_Wyler ≈ 137.0360824481643
CODATA 2018: α⁻¹ = 137.035999084(21)
Deviation: |137.0360824 137.035999084| ≈ 8.34 × 10⁻⁵
**SPECULATIVE** — agreement is numerological; no physical derivation established.
-/
def wylerAlphaInverseTrue : Float :=
let alphaCoupling : Float :=
(9.0 / (8.0 * floatPi ^ 4)) * ((floatPi ^ 5 / (16.0 * 120.0)) ^ (1.0 / 4.0))
1.0 / alphaCoupling
/--
The CODATA 2018 accepted value of α⁻¹ used as the reference for deviation checks.
α⁻¹_CODATA = 137.035999084(21)
-/
def codataAlphaInverse : Float := 137.035999084
/--
Deviation of `wylerAlphaInverseTrue` from the CODATA value:
Δ = wylerAlphaInverseTrue codataAlphaInverse
Expected: ≈ +8.34 × 10⁻⁵
-/
def wylerDeviation : Float :=
wylerAlphaInverseTrue - codataAlphaInverse
-- ═══════════════════════════════════════════════════════════════════
-- §3 Recamán + Gap-6 Candidate (SPECULATIVE)
-- ═══════════════════════════════════════════════════════════════════
/--
`recamanGap6Candidate` is the HCMMR-native candidate for α⁻¹:
α⁻¹_candidate = R(122) + Δ_gap6
= 137 + 1/28
≈ 137.03571...
where:
- R(122) = 137 is the Recamán sequence value at index 122.
- Δ_gap6 = 1/(4 × 7) = 1/28 is the proposed gap-6 self-linking correction
(p₁ = 4, p₂ = 7, the gap-6 sentinel primes from the prime lane structure).
Deviation from CODATA:
|137.03571 137.035999| / 137.035999 ≈ 2.1 × 10⁻⁶
**SPECULATIVE.** No formal coupling rule connects R(122) or Δ_gap6 to the
electromagnetic coupling. The Recamán sequence contains every positive integer
(conjectured), so R(n) = 137 for some n; the significance of n = 122 is unknown.
See: ChatLog_Math_Synthesis_2026-05-11.md §3.4, §4.2
-/
def recamanGap6Candidate : Float :=
137.0 + (1.0 / 28.0)
/-- Deviation of the Recamán/gap-6 candidate from CODATA. -/
def recamanDeviation : Float :=
recamanGap6Candidate - codataAlphaInverse
-- ═══════════════════════════════════════════════════════════════════
-- §4 Q16_16 Cross-Check
-- ═══════════════════════════════════════════════════════════════════
/--
The HCMMR Q16_16 anchor value for α⁻¹:
alpha_inverse = ⟨8980791⟩ = 137.036 × 65536
This is copied from `Law18_Constants.anchorConstants` for local reference.
The fixed-point representation stores α⁻¹ to 3 decimal places.
Relationship to Float computation:
anchorValue / 65536 = 8980791 / 65536 ≈ 137.036011...
wylerAlphaInverseTrue ≈ 137.036082...
codataAlphaInverse = 137.035999...
All three agree within 10⁻⁴ (well within Q16_16 fixed-point resolution of ~1.5×10⁻⁵).
-/
def alphaInverseQ16_16Anchor : Semantics.FixedPoint.Q16_16 := ⟨8980791⟩
/--
Float value recovered from the Q16_16 anchor: 8980791 / 65536.
-/
def alphaInverseFromAnchor : Float :=
8980791.0 / 65536.0
/-- Deviation of the Q16_16 anchor from CODATA (Float). -/
def anchorDeviation : Float :=
alphaInverseFromAnchor - codataAlphaInverse
-- ═══════════════════════════════════════════════════════════════════
-- §5 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- §5.1 Canonical Wyler structure instance
-- Expected: { numeratorCoeff := 9, piPower4Denom := 4, innerPiPower := 5,
-- innerDenom := 1920, rootOrder := 4 }
#eval canonicalWyler
-- §5.2 Raw expression (9/(8π⁴)) × (π⁵/(16×120)) — per task specification
-- Expected: ≈ 0.001840776945... (this is NOT α⁻¹; it is 9π/(8×1920))
-- NOTE: The reciprocal of this value is ≈ 543.25, also not α⁻¹.
#eval wylerAlphaInverse
-- §5.3 Reciprocal of the raw expression (for completeness)
-- Expected: ≈ 543.248...
#eval (1.0 / wylerAlphaInverse : Float)
-- §5.4 Wyler α⁻¹ with the correct ¼-power root
-- Expected: ≈ 137.036082...
-- Verified: (9/(8π⁴)) × (π⁵/1920)^(1/4) then inverted
#eval wylerAlphaInverseTrue
-- §5.5 Deviation from CODATA 2018 (α⁻¹ = 137.035999084)
-- Expected: ≈ +8.34 × 10⁻⁵
#eval wylerDeviation
-- §5.6 Recamán + gap-6 candidate
-- Expected: ≈ 137.035714... (= 137 + 1/28)
#eval recamanGap6Candidate
-- §5.7 Recamán deviation from CODATA
-- Expected: ≈ 2.85 × 10⁻⁴
#eval recamanDeviation
-- §5.8 Q16_16 anchor recovered as Float
-- Expected: ≈ 137.036011...
#eval alphaInverseFromAnchor
-- §5.9 Q16_16 anchor deviation from CODATA
-- Expected: ≈ +1.22 × 10⁻⁵
#eval anchorDeviation
-- §5.10 Summary table (all three estimates vs CODATA)
#eval do
let codata := codataAlphaInverse
let wyler := wylerAlphaInverseTrue
let recaman := recamanGap6Candidate
let anchor := alphaInverseFromAnchor
IO.println s!"=== α⁻¹ Estimates vs CODATA 2018 ==="
IO.println s!"CODATA 2018 : {codata}"
IO.println s!"Wyler (true): {wyler} Δ = {wyler - codata}"
IO.println s!"Recamán+1/28: {recaman} Δ = {recaman - codata}"
IO.println s!"Q16_16 anchor: {anchor} Δ = {anchor - codata}"
IO.println s!"Raw Wyler form (NOT α⁻¹): {wylerAlphaInverse}"
end Semantics.HCMMR.Law18Alpha

View file

@ -0,0 +1,346 @@
/-
Law 18 — Scale/Constant Anchoring
HCMMR does not predict constants as raw numbers (they're dimensionful and
unit-dependent). It recovers their *roles* as limiting calibration constants
and tests **dimensionless** outputs. The canonical equation includes Ω_K
(Constant Calibration Gate) as a multiplicative factor.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law18
Import: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law18
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Calibration Constants (anchored, not predicted)
-- ═══════════════════════════════════════════════════════════════════
/--
A collection of physical constants used as calibration anchors.
HCMMR does not predict these as raw numbers — it uses them as known
references to calibrate its dimensionless output tests. Each constant
is stored as a scaled Q16_16 value.
-/
structure CalibrationGate where
alpha_inverse : Q16_16
pi : Q16_16
tau : Q16_16
phi : Q16_16
e_natural : Q16_16
speedOfLight : Q16_16
planckConstant : Q16_16
boltzmann : Q16_16
gravitational : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Returns a CalibrationGate populated with known NIST/CODATA values
as scaled Q16_16 fixed-point representations.
Constants are scaled to fit within Q16_16 range:
c → c / 10⁸ (speedOfLight)
ℏ → ℏ / 10⁻³⁴ (planckConstant)
k_B → k_B / 10⁻²³ (boltzmann)
G → G / 10⁻¹¹ (gravitational)
-/
def anchorConstants : CalibrationGate :=
{ alpha_inverse := ⟨8980791⟩ -- 137.036 × 65536
, pi := ⟨205887⟩ -- 3.14159 × 65536
, tau := ⟨411775⟩ -- 6.28319 × 65536
, phi := ⟨106039⟩ -- 1.61803 × 65536
, e_natural := ⟨178139⟩ -- 2.71828 × 65536
, speedOfLight := ⟨196470⟩ -- 2.99792 × 65536
, planckConstant := ⟨69115⟩ -- 1.05457 × 65536
, boltzmann := ⟨90494⟩ -- 1.38065 × 65536
, gravitational := ⟨437412⟩ -- 6.67430 × 65536
}
/--
Computes a composite health score for a CalibrationGate.
All constants must be non-zero and within their known ranges.
Returns 1.0 if all constants are correctly anchored, 0.0 otherwise.
-/
def calibrationScore (g : CalibrationGate) : Q16_16 :=
let ranges : List (Q16_16 × Q16_16 × Q16_16) :=
[ (g.alpha_inverse, ⟨8912896⟩, ⟨9043968⟩) -- 136 .. 138
, (g.pi, ⟨203162⟩, ⟨209715⟩) -- 3.1 .. 3.2
, (g.tau, ⟨406323⟩, ⟨419430⟩) -- 6.2 .. 6.4
, (g.phi, ⟨104858⟩, ⟨111411⟩) -- 1.6 .. 1.7
, (g.e_natural, ⟨170394⟩, ⟨183501⟩) -- 2.6 .. 2.8
, (g.speedOfLight, ⟨183501⟩, ⟨209715⟩) -- 2.8 .. 3.2
, (g.planckConstant, ⟨58982⟩, ⟨78643⟩) -- 0.9 .. 1.2
, (g.boltzmann, ⟨58982⟩, ⟨98304⟩) -- 0.9 .. 1.5
, (g.gravitational, ⟨425984⟩, ⟨491520⟩) -- 6.5 .. 7.5
]
let allOk := ranges.all (fun (v, lo, hi) =>
v.val != 0 && v.val >= lo.val && v.val <= hi.val)
if allOk then Q16_16.one else Q16_16.zero
-- ═══════════════════════════════════════════════════════════════════
-- §2 Dimensionless Output Tests
-- ═══════════════════════════════════════════════════════════════════
/--
Records a dimensionless model output test:
name — identifier (e.g. "fine_structure")
predicted — model-computed value
experimental— measured/reference value
residual — |predicted experimental| / experimental
-/
structure DimensionlessOutput where
name : String
predicted : Q16_16
experimental : Q16_16
residual : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
ε_K = |log(predicted / experimental)|
Log-ratio dimensionless residual. Returns 0 when predicted equals
experimental, positive otherwise.
-/
def residualLogRatio (d : DimensionlessOutput) : Q16_16 :=
let ratio := Q16_16.div d.predicted d.experimental
if ratio.val == 0 || ratio.toInt <= 0 then Q16_16.zero
else Q16_16.abs (Q16_16.log2 ratio)
/--
Tests whether the model's fine-structure constant inverse is within
±1% of the accepted value α⁻¹ ≈ 137.036.
Returns the fractional residual |α_pred α_exp| / α_exp.
-/
def fineStructureTest (alpha : Q16_16) : Q16_16 :=
let expected : Q16_16 := ⟨8980791⟩ -- 137.036
let diff := Q16_16.abs (Q16_16.sub alpha expected)
Q16_16.div diff expected
/--
Tests the proton-to-electron mass ratio ≈ 1836.15.
Returns the fractional residual |m_pred m_exp| / m_exp.
-/
def massRatioTest (massRatio : Q16_16) : Q16_16 :=
let expected : Q16_16 := ⟨120335077⟩ -- 1836.15 × 65536
if expected.val == 0 then Q16_16.zero
else
let diff := Q16_16.abs (Q16_16.sub massRatio expected)
Q16_16.div diff expected
/--
Tests the Planck-length scale via √(ℏG/c^3) against the expected
scaled Planck length ≈ 1.616e-35 m (scaled into Q16_16 range).
Computes the dimensionless fractional residual.
-/
def planckRatioTest (hbar : Q16_16) (G : Q16_16) (c : Q16_16) : Q16_16 :=
let c3 := Q16_16.mul (Q16_16.mul c c) c
if c3.val == 0 then Q16_16.one
else
let product := Q16_16.mul hbar G
let lp := Q16_16.sqrt (Q16_16.div product c3)
let expected : Q16_16 := ⟨33509⟩ -- 0.5111 × 65536 (scaled Planck length)
if expected.val == 0 then Q16_16.one
else
let diff := Q16_16.abs (Q16_16.sub lp expected)
Q16_16.div diff expected
/--
Constructs a dimensionless test gate from a name and residual.
Verdict: admit if residual ≤ 1%, hold if ≤ 5%, reject otherwise.
Score saturates at 1.0 residual on [0,1].
-/
def dimensionlessTestGate (name : String) (residual : Q16_16) : Gate :=
let score := Q16_16.sat01 (Q16_16.sub Q16_16.one residual)
let threshold01 : Q16_16 := ⟨655⟩ -- 0.01
let threshold05 : Q16_16 := ⟨3277⟩ -- 0.05
let verdict :=
if residual.val <= threshold01.val then GateVerdict.admit
else if residual.val <= threshold05.val then GateVerdict.hold
else GateVerdict.reject
{ name := name, required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §3 Omega-K Gate
-- ═══════════════════════════════════════════════════════════════════
/--
Multiplicative calibration score: returns 1.0 if all constants are
non-zero, 0.0 if any is missing (zero literal).
-/
def omegaKScore (g : CalibrationGate) : Q16_16 :=
let allNonZero :=
g.alpha_inverse.val != 0 && g.pi.val != 0 && g.tau.val != 0 &&
g.phi.val != 0 && g.e_natural.val != 0 && g.speedOfLight.val != 0 &&
g.planckConstant.val != 0 && g.boltzmann.val != 0 &&
g.gravitational.val != 0
if allNonZero then Q16_16.one else Q16_16.zero
/--
Ω_K = Ω_π × Ω_τ × Ω_φ × Ω_e × Ω_c × Ω_ℏ × Ω_kB × Ω_α × Ω_G
Each sub-factor is 1.0 if the constant is correctly anchored, 0.0 otherwise.
Verdict: admit if all anchored, hold if some approximated (non-zero but out of
range), reject if any is missing/zero.
-/
def omegaKGate (g : CalibrationGate) : Gate :=
let score := omegaKScore g
let calScore := calibrationScore g
let verdict :=
if score.val == 0 then GateVerdict.reject
else if calScore.val == Q16_16.one.val then GateVerdict.admit
else GateVerdict.hold
{ name := "ConstantCalibration", required := true, score := score, verdict := verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §4 Constant Recovery Gate (full law)
-- ═══════════════════════════════════════════════════════════════════
/--
Builds the full constant-recovery GateChain from a CalibrationGate.
Combines:
1. Calibration anchoring check (omegaKGate)
2. Fine-structure test (α⁻¹ ≈ 137.036)
3. Mass-ratio test (m_p/m_e ≈ 1836.15)
4. Planck-ratio test (√(ℏG/c^3))
-/
def constantRecoveryGate (g : CalibrationGate) : GateChain :=
let fsResidual := fineStructureTest g.alpha_inverse
let mrResidual := massRatioTest (Q16_16.ofInt 1836)
let prResidual := planckRatioTest g.planckConstant g.gravitational g.speedOfLight
{ gates :=
[ omegaKGate g
, dimensionlessTestGate "FineStructure" fsResidual
, dimensionlessTestGate "MassRatio" mrResidual
, dimensionlessTestGate "PlanckRatio" prResidual
]
}
/--
Evaluates constantRecoveryGate via gateChainVerdict.
Returns the composite GateVerdict for the full law.
-/
def constantRecoveryVerdict (g : CalibrationGate) : GateVerdict :=
gateChainVerdict (constantRecoveryGate g)
-- ═══════════════════════════════════════════════════════════════════
-- §5 Fixtures
-- ═══════════════════════════════════════════════════════════════════
/-- CalibrationGate with CODATA 2022 approximate values. -/
def coDataCalibrationFixture : CalibrationGate := anchorConstants
/-- Broken CalibrationGate: speedOfLight = 0 (photon missing). -/
def missingPhotonFixture : CalibrationGate :=
{ coDataCalibrationFixture with speedOfLight := Q16_16.zero }
/-- DimensionlessOutput for fine-structure constant with matched values. -/
def fineStructureFixture : DimensionlessOutput :=
let val : Q16_16 := ⟨8980791⟩
let res : Q16_16 := Q16_16.zero
{ name := "fine_structure", predicted := val, experimental := val, residual := res }
/--
CalibrationGate where all constants are anchored with in-range values,
suitable for theorem witnessing.
-/
def anchoredCalibrationFixture : CalibrationGate :=
{ alpha_inverse := Q16_16.ofInt 137
, pi := ⟨205887⟩
, tau := ⟨411775⟩
, phi := ⟨106039⟩
, e_natural := ⟨178139⟩
, speedOfLight := Q16_16.ofInt 3
, planckConstant := Q16_16.ofInt 1
, boltzmann := Q16_16.ofInt 1
, gravitational := Q16_16.ofInt 7
}
-- ═══════════════════════════════════════════════════════════════════
-- §6 Theorems
-- ═══════════════════════════════════════════════════════════════════
/--
When all constants are non-zero and within range, omegaKGate admits.
-/
theorem omegaK_admits_anchored :
(omegaKGate anchoredCalibrationFixture).verdict = GateVerdict.admit := by
native_decide
/--
When any constant is zero, omegaKScore is 0.
-/
theorem omegaK_rejects_missing :
omegaKScore missingPhotonFixture = Q16_16.zero := by
native_decide
/--
When predicted equals experimental, the dimensionless residual is zero.
-/
theorem dimensionless_zero_residual_on_exact :
fineStructureFixture.residual = Q16_16.zero := by
native_decide
/--
Anchored constants yield calibration score 1.0.
-/
theorem calibration_anchored_score_one :
calibrationScore anchoredCalibrationFixture = Q16_16.one := by
native_decide
-- ═══════════════════════════════════════════════════════════════════
-- §7 #eval Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- Calibration constants
#eval anchorConstants
#eval coDataCalibrationFixture
#eval missingPhotonFixture
#eval anchoredCalibrationFixture
-- Calibration scoring
#eval calibrationScore coDataCalibrationFixture
#eval calibrationScore missingPhotonFixture
#eval calibrationScore anchoredCalibrationFixture
-- Omega-K gate
#eval omegaKScore coDataCalibrationFixture
#eval omegaKScore missingPhotonFixture
#eval omegaKGate coDataCalibrationFixture
#eval omegaKGate missingPhotonFixture
#eval omegaKGate anchoredCalibrationFixture
-- Dimensionless output tests
#eval fineStructureFixture
#eval residualLogRatio fineStructureFixture
#eval fineStructureTest coDataCalibrationFixture.alpha_inverse
#eval massRatioTest (Q16_16.ofInt 1836)
#eval planckRatioTest coDataCalibrationFixture.planckConstant
coDataCalibrationFixture.gravitational
coDataCalibrationFixture.speedOfLight
-- Dimensionless test gates
#eval dimensionlessTestGate "FineStructure" (fineStructureTest coDataCalibrationFixture.alpha_inverse)
#eval dimensionlessTestGate "MassRatio" (massRatioTest (Q16_16.ofInt 1836))
-- Full constant recovery
#eval constantRecoveryGate coDataCalibrationFixture
#eval constantRecoveryGate missingPhotonFixture
#eval constantRecoveryGate anchoredCalibrationFixture
#eval constantRecoveryVerdict coDataCalibrationFixture
#eval constantRecoveryVerdict missingPhotonFixture
#eval constantRecoveryVerdict anchoredCalibrationFixture
end Semantics.HCMMR.Law18

View file

@ -0,0 +1,418 @@
/-
Law 19 — VoidScar Fractal Field & Regime Gate
Encodes three primitives derived from the Menger/Koch/DESI synthesis
(see `6-Documentation/docs/distilled/ObserverScale_RegimeGate_VoidScar.md`):
1. **VoidScar fractal constants** — Koch boundary dimension ln(4)/ln(3) and the
Menger/Koch divergence pressure ratio (9/5)^n, complementing the Menger
Hausdorff dimension already in Law18_Constants and MengerSpongeFractalAddressing.
2. **VoidScarField** — a paired (Ω_void, R_scar) structure capturing interior
void pressure and boundary scar residual, with an admissibility gate that
detects Koch-class divergence (boundary cost exceeding void scaffold).
3. **RegimeGate** — the "active physics" operator A_r that determines which
law class is awake at a given energy/coupling scale. Encodes the insight
that the same geometric action (a fist, a gaze vector, a flying body) can
belong to different physics charts depending on cumulative energy deposition.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law19
Import: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law19
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Fractal Dimension Constants
-- ═══════════════════════════════════════════════════════════════════
/--
Koch boundary fractal dimension: D_K = ln(4)/ln(3) ≈ 1.26186.
Scaled to Q16_16: 1.26186 × 65536 = 82,706.
Verified: Wolfram Alpha query `log(4)/log(3)` → 1.26185950...
-/
def kochBoundaryDim : Q16_16 := ⟨82706⟩
/--
Menger sponge Hausdorff dimension: D_M = ln(20)/ln(3) ≈ 2.72683.
Cross-reference: Law18_Constants anchorConstants and
MengerSpongeFractalAddressing.lean §0 store this as ⟨17910⟩ in a
per-module Q16_16 convention. Here we store the full-precision value
at the standard 65536 scale: 2.72683 × 65536 = 178,696.
Verified: Wolfram Alpha `log(20)/log(3)` → 2.72683...
-/
def mengerVoidDim : Q16_16 := ⟨178696⟩
/--
Menger/Koch divergence pressure numerator: 9 (from ratio 9/5).
The boundary-to-interior divergence ratio per iteration step is
D_MK = (4/3)^n / (20/27)^n = (4/3 × 27/20)^n = (9/5)^n.
Numerator stored separately to avoid fixed-point overflow in
iterated multiplication.
-/
def mkDivNumerator : Q16_16 := ⟨589824⟩ -- 9 × 65536
/--
Menger/Koch divergence pressure denominator: 5.
-/
def mkDivDenominator : Q16_16 := ⟨327680⟩ -- 5 × 65536
/--
One step of the Menger/Koch divergence ratio: D_MK(1) = 9/5 = 1.8.
Scaled: 1.8 × 65536 = 117,964.
Verified: Wolfram Alpha `9/5` = 1.8
-/
def mkDivOneStep : Q16_16 := ⟨117964⟩
-- ═══════════════════════════════════════════════════════════════════
-- §2 VoidScarField — paired interior/boundary pressure structure
-- ═══════════════════════════════════════════════════════════════════
/--
A VoidScarField pairs the interior void pressure (Ω_void, Menger-side)
with the boundary scar residual (R_scar, Koch-side).
omegaVoid — surviving volumetric scaffold; decreases as recursion deepens
rScar — boundary scar cost; increases as recursion deepens
epsilon — regularisation floor preventing divide-by-zero in D_MK
depth — recursion depth n at which this snapshot was taken
The field is admissible when scar cost does not bankrupt void savings:
R_scar ≤ omega_void (see `voidScarAdmissible`)
-/
structure VoidScarField where
omegaVoid : Q16_16
rScar : Q16_16
epsilon : Q16_16
depth : Nat
deriving Repr, BEq, DecidableEq, Inhabited
/--
Default VoidScarField: unit void, zero scar, standard epsilon, depth 0.
-/
def VoidScarField.default : VoidScarField :=
{ omegaVoid := Q16_16.one
, rScar := Q16_16.zero
, epsilon := Q16_16.epsilon
, depth := 0
}
/--
Divergence pressure at this field snapshot:
D_MK = R_scar / (omegaVoid + epsilon)
Returns a dimensionless ratio in Q16_16.
Values above Q16_16.one indicate Koch-class divergence.
-/
def voidScarDivergence (f : VoidScarField) : Q16_16 :=
let denom := Q16_16.add f.omegaVoid f.epsilon
if denom.val == 0 then Q16_16.infinity
else Q16_16.div f.rScar denom
/--
Admissibility test: the field is admissible when boundary scar cost
does not exceed the surviving void scaffold.
admissible ⟺ R_scar ≤ omegaVoid
-/
def voidScarAdmissible (f : VoidScarField) : Bool :=
f.rScar.val <= f.omegaVoid.val
/--
One Menger deletion step: reduces omegaVoid by factor 20/27.
Scaled: 20/27 × 65536 = 48,560.
Verified: Wolfram Alpha `(20/27)*65536` → 48560.59... → floor 48560.
-/
def mengerDeleteStep (f : VoidScarField) : VoidScarField :=
let factor : Q16_16 := ⟨48560⟩
{ f with
omegaVoid := Q16_16.div (Q16_16.mul f.omegaVoid factor) Q16_16.one
, depth := f.depth + 1
}
/--
One Koch boundary growth step: multiplies rScar by factor 4/3.
Scaled: 4/3 × 65536 = 87,381.
Verified: Wolfram Alpha `(4/3)*65536` → 87381.33... → floor 87381.
-/
def kochScarStep (f : VoidScarField) : VoidScarField :=
let factor : Q16_16 := ⟨87381⟩
{ f with
rScar := Q16_16.div (Q16_16.mul f.rScar factor) Q16_16.one
, depth := f.depth + 1
}
/--
Combined void/scar step: apply one Menger deletion and one Koch growth.
-/
def voidScarStep (f : VoidScarField) : VoidScarField :=
kochScarStep (mengerDeleteStep f)
/--
Gate verdict for a VoidScarField based on its divergence pressure:
D_MK ≤ 1.0 → admit (scar within scaffold)
D_MK ≤ 1.8 → hold (one-step pressure, Koch boundary catching up)
D_MK > 1.8 → reject (Koch divergence exceeds Menger support)
-/
def voidScarGate (f : VoidScarField) : Gate :=
let d := voidScarDivergence f
let oneStep : Q16_16 := mkDivOneStep -- 1.8 threshold
let verdict :=
if d.val <= Q16_16.one.val then GateVerdict.admit
else if d.val <= oneStep.val then GateVerdict.hold
else GateVerdict.reject
let score :=
if d.val == 0 then Q16_16.one
else Q16_16.sat01 (Q16_16.div Q16_16.one d)
{ name := "VoidScar", required := true, score := score, verdict := verdict }
-- #eval to verify arithmetic
-- Expect: admit (rScar 0, omegaVoid 1 → D_MK = 0)
#eval (voidScarGate VoidScarField.default).verdict
-- Expect: reject (rScar > omegaVoid after 3 steps from seeded field)
#eval
let seeded : VoidScarField := { VoidScarField.default with rScar := Q16_16.one }
let stepped := voidScarStep (voidScarStep (voidScarStep seeded))
(voidScarGate stepped).verdict
-- ═══════════════════════════════════════════════════════════════════
-- §3 RegimeGate — active-physics operator
-- ═══════════════════════════════════════════════════════════════════
/--
The physics regime active at a given scale.
Regimes are ordered by cumulative energy / coupling density.
The same geometric action occupies different charts at different
energies — a fist punch vs a Hulk punch; Superman vs Omni-Man
(suppressed coupling vs admitted coupling); Cyclops' gaze as
information-intake vs momentum-transfer.
Formal reference:
A_r = Gate(E, p, Δt, A, σ, ρ, c_s, ε_deposit, Θ_medium)
-/
inductive PhysicsRegime where
| elastic -- stress below yield; deformation recovers
| plastic -- stress above yield; permanent deformation
| fracture -- crack/fragmentation network propagates
| shock -- impulse faster than acoustic relaxation (v > c_s)
| thermal -- energy density drives phase transition
| plasma -- ionisation / extreme energy density
deriving Repr, BEq, DecidableEq, Inhabited
/--
RegimeGate: captures the inputs that determine which PhysicsRegime is active.
energyDensity — E/V, energy per unit volume (Q16_16, scaled)
impulseRate — p/Δt, rate of momentum transfer
couplingEta — η_deposit ∈ [0,1], fraction of kinetic energy
deposited into the medium (1 = full coupling,
0 = suppressed coupling as in Superman flight)
yieldThreshold — σ_y, material yield stress threshold
acousticLimit — c_s, speed of sound in medium (for shock gate)
-/
structure RegimeGate where
energyDensity : Q16_16
impulseRate : Q16_16
couplingEta : Q16_16 -- dimensionless, Q16_16 [0,1]
yieldThreshold : Q16_16
acousticLimit : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Resolves the active PhysicsRegime from a RegimeGate.
Ordered threshold checks (first match wins):
1. impulseRate > acousticLimit × couplingEta → shock
2. energyDensity > 8 × yieldThreshold → plasma (extreme)
3. energyDensity > 4 × yieldThreshold → thermal
4. energyDensity > 2 × yieldThreshold → fracture
5. energyDensity > yieldThreshold → plastic
6. otherwise → elastic
-/
def resolveRegime (g : RegimeGate) : PhysicsRegime :=
let acousticCoupled := Q16_16.div (Q16_16.mul g.acousticLimit g.couplingEta) Q16_16.one
if g.impulseRate.val > acousticCoupled.val then
PhysicsRegime.shock
else
let thr2 := Q16_16.mul g.yieldThreshold ⟨131072⟩ -- × 2
let thr4 := Q16_16.mul g.yieldThreshold ⟨262144⟩ -- × 4
let thr8 := Q16_16.mul g.yieldThreshold ⟨524288⟩ -- × 8
if g.energyDensity.val > thr8.val then PhysicsRegime.plasma
else if g.energyDensity.val > thr4.val then PhysicsRegime.thermal
else if g.energyDensity.val > thr2.val then PhysicsRegime.fracture
else if g.energyDensity.val > g.yieldThreshold.val then PhysicsRegime.plastic
else PhysicsRegime.elastic
/--
Coupling class for an observer/actor axis.
"You are here" in regime space: the same projection axis (gaze vector,
motion vector, contact surface) belongs to a different coupling class
depending on how much energy it deposits into the medium.
passive — information intake only (η ≈ 0; normal observer gaze)
kinematic — sub-threshold momentum transfer (typical motion)
concussive — above-threshold impulse transfer (Cyclops optic blast;
canonical Marvel description: heatless concussive force)
destructive — energy density exceeds medium admissibility
-/
inductive CouplingClass where
| passive
| kinematic
| concussive
| destructive
deriving Repr, BEq, DecidableEq, Inhabited
/--
Resolves the CouplingClass from a RegimeGate.
Thresholds (on couplingEta × energyDensity composite):
deposited = couplingEta × energyDensity
> 2 × yieldThreshold → destructive
> yieldThreshold → concussive
> yieldThreshold/4 → kinematic
otherwise → passive
-/
def resolveCoupling (g : RegimeGate) : CouplingClass :=
let deposited := Q16_16.div (Q16_16.mul g.couplingEta g.energyDensity) Q16_16.one
let thr2 := Q16_16.mul g.yieldThreshold ⟨131072⟩ -- × 2
let thr4 := Q16_16.div g.yieldThreshold ⟨262144⟩ -- ÷ 4
if deposited.val > thr2.val then CouplingClass.destructive
else if deposited.val > g.yieldThreshold.val then CouplingClass.concussive
else if deposited.val > thr4.val then CouplingClass.kinematic
else CouplingClass.passive
/--
Builds a Gate from a RegimeGate for inclusion in a GateChain.
A regime gate admits when the active regime is elastic or kinematic
(low-coupling, stable physics). It holds at plastic/concussive
(approaching threshold). It rejects at fracture/shock/thermal/plasma/destructive.
-/
def regimeGateVerdict (g : RegimeGate) : Gate :=
let regime := resolveRegime g
let coupling := resolveCoupling g
let verdict :=
match regime, coupling with
| PhysicsRegime.elastic, CouplingClass.passive => GateVerdict.admit
| PhysicsRegime.elastic, CouplingClass.kinematic => GateVerdict.admit
| PhysicsRegime.plastic, _ => GateVerdict.hold
| _, CouplingClass.concussive => GateVerdict.hold
| _, _ => GateVerdict.reject
let score : Q16_16 :=
match verdict with
| GateVerdict.admit => Q16_16.one
| GateVerdict.hold => ⟨32768⟩ -- 0.5
| GateVerdict.reject => Q16_16.zero
{ name := "RegimeGate", required := true, score := score, verdict := verdict }
-- #eval witnesses
-- Low-energy elastic case → expect admit
#eval
let g : RegimeGate :=
{ energyDensity := ⟨1000⟩
, impulseRate := ⟨500⟩
, couplingEta := ⟨655⟩ -- ≈ 0.01, suppressed coupling
, yieldThreshold := ⟨65536⟩ -- = 1.0
, acousticLimit := ⟨196608⟩ -- = 3.0
}
(regimeGateVerdict g).verdict
-- Hulk-punch case: high energy, full coupling → expect reject
#eval
let g : RegimeGate :=
{ energyDensity := ⟨524288⟩ -- = 8.0, above 8× threshold
, impulseRate := ⟨65536⟩
, couplingEta := Q16_16.one -- full coupling
, yieldThreshold := ⟨65536⟩
, acousticLimit := ⟨196608⟩
}
(regimeGateVerdict g).verdict
-- Cyclops case: passive energy density but concussive coupling class
-- (η is high, deposited > threshold) → expect hold (concussive branch)
#eval
let g : RegimeGate :=
{ energyDensity := ⟨131072⟩ -- = 2.0
, impulseRate := ⟨1000⟩
, couplingEta := Q16_16.one -- full coupling (gaze = force vector)
, yieldThreshold := ⟨65536⟩
, acousticLimit := ⟨655360⟩ -- = 10.0, well above impulseRate
}
(regimeGateVerdict g).verdict
-- ═══════════════════════════════════════════════════════════════════
-- §4 Combined VoidScar + Regime GateChain
-- ═══════════════════════════════════════════════════════════════════
/--
Builds a GateChain combining void/scar admissibility with regime stability.
A HCMMR object is lawful at a given scale only if:
(a) its boundary scar does not bankrupt the void scaffold, AND
(b) the active physics regime is below the fracture/shock threshold.
-/
def voidScarRegimeChain (f : VoidScarField) (r : RegimeGate) : GateChain :=
{ gates := [voidScarGate f, regimeGateVerdict r] }
-- ═══════════════════════════════════════════════════════════════════
-- §5 Divergence Class Enumeration
-- ═══════════════════════════════════════════════════════════════════
/--
The three divergence classes identified in the VoidScar synthesis.
These classify failure modes that previously appeared as undifferentiated
"model blow-up" events.
-/
inductive DivergenceClass where
| mengerCollapse -- interior deletion too aggressive; V_n → 0
| kochExplosion -- boundary complexity exceeds receipt capacity; L_n → ∞
| chartMismatch -- different observer projections cut at incompatible scales
deriving Repr, BEq, DecidableEq, Inhabited
/--
Classifies the divergence of a VoidScarField.
omegaVoid ≤ epsilon → mengerCollapse
rScar > omegaVoid × mkDivOneStep → kochExplosion
otherwise (structurally coherent) → chartMismatch (projection issue)
-/
def classifyDivergence (f : VoidScarField) : Option DivergenceClass :=
if f.omegaVoid.val <= f.epsilon.val then
some DivergenceClass.mengerCollapse
else
let kochThreshold := Q16_16.div (Q16_16.mul f.omegaVoid mkDivOneStep) Q16_16.one
if f.rScar.val > kochThreshold.val then
some DivergenceClass.kochExplosion
else if not (voidScarAdmissible f) then
some DivergenceClass.chartMismatch
else
none -- no divergence
-- #eval: collapsed void → mengerCollapse
#eval classifyDivergence { VoidScarField.default with omegaVoid := Q16_16.epsilon }
-- #eval: rScar >> omegaVoid → kochExplosion
#eval classifyDivergence { omegaVoid := Q16_16.one, rScar := ⟨200000⟩, epsilon := Q16_16.epsilon, depth := 3 }
-- #eval: balanced field → none
#eval classifyDivergence VoidScarField.default
end Semantics.HCMMR.Law19

View file

@ -0,0 +1,494 @@
/-
Law 20 — Shockwave / Front Gate
Formalises the HCMMR discontinuity-handling gate A_shock.
Doctrine: a discontinuity (shockwave, contact front, phase boundary) is NOT
a failure of physics. It is a *gate event* with a typed receipt that captures:
1. **Hyperbolicity** — the PDE system is hyperbolic, so characteristic speeds
exist and information propagates at finite velocity. Non-hyperbolic objects
are rejected (Underverse entry) before any shock processing.
2. **RankineHugoniot jump relations** — across the front, mass, momentum, and
energy flux must balance. The residual ε_RH measures how far the candidate
state diverges from exact balance.
3. **Entropy (Lax) admissibility condition** — the shock is physically admissible
only if entropy *increases* across the front (2nd-law arrow). Entropy-
decreasing "expansion shocks" are routed to the Underverse as inadmissible.
4. **Causal front constraint** — the front speed s satisfies
u_L c_L ≤ s ≤ u_R + c_R (CFL-sound-speed envelope)
Fronts exceeding the causal envelope are rejected with a speed-excess residual.
5. **Irreversibility receipt** — every admitted shock emits a typed receipt
recording the jump deltas, entropy gain, characteristic speeds, and
causal-validity flag. These feed back into Law 16 (Entropy/Heat Leak) as
Underverse scar contributions.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law20
Imports: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law20
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Fixed-point arithmetic helpers
-- All intermediate arithmetic is done in Nat (arbitrary precision)
-- and then clamped back to UInt32 for Q16_16.val.
-- ═══════════════════════════════════════════════════════════════════
private def toN (q : Q16_16) : Nat := q.val.toNat
/--
Q16_16 subtraction clamped to zero (no wrap-around for unsigned-like use).
-/
private def q_sub (a b : Q16_16) : Q16_16 :=
let an := toN a; let bn := toN b
if an ≥ bn then ⟨(an - bn).toUInt32⟩ else ⟨0⟩
/--
Absolute difference of two Q16_16 values — always non-negative.
-/
private def q_absdiff (a b : Q16_16) : Q16_16 :=
let an := toN a; let bn := toN b
if an ≥ bn then ⟨(an - bn).toUInt32⟩ else ⟨(bn - an).toUInt32⟩
/--
Q16_16 addition, saturating at UInt32.max to avoid overflow.
-/
private def q_add (a b : Q16_16) : Q16_16 :=
let s := toN a + toN b
⟨(min s 0xFFFFFFFF).toUInt32⟩
/--
Q16_16 scaled division: (a × 65536) / b in Nat, clamped to UInt32.
Returns ⟨0⟩ if b = 0.
-/
private def q_div (a b : Q16_16) : Q16_16 :=
let bn := toN b
if bn = 0 then ⟨0⟩ else ⟨(min ((toN a * 65536) / bn) 0xFFFFFFFF).toUInt32⟩
-- ═══════════════════════════════════════════════════════════════════
-- §2 Primitive State Vectors
-- ═══════════════════════════════════════════════════════════════════
/--
A one-dimensional conserved-variable state on one side of a discontinuity.
Fields are stored as Q16_16 scaled values:
- `density` : ρ (kg m⁻³ × 65536, clipped to fit Q16_16)
- `velocity` : u (m s⁻¹ × 65536 / 1000 → per-km/s units)
- `pressure` : p (Pa × 65536 / 10⁵ → per-bar units)
- `energy` : e (J kg⁻¹ × 65536 / 10⁶ → per-MJ/kg units)
- `soundSpd` : c_s (m s⁻¹ × 65536 / 1000 → per-km/s units)
The internal scales are self-consistent for residual comparison; no SI
conversion is needed inside the gate. The gate only needs ratios and differences.
-/
structure FluidState where
density : Q16_16
velocity : Q16_16
pressure : Q16_16
energy : Q16_16
soundSpd : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
A discontinuity event: left state, right state, and the front propagation speed.
`frontSpeed` is signed via the convention that positive means rightward propagation.
Stored in the same per-km/s units as `velocity`.
-/
structure ShockEvent where
stateL : FluidState
stateR : FluidState
frontSpeed : Q16_16 -- |s| in per-km/s units
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §3 Hyperbolicity Gate
-- ═══════════════════════════════════════════════════════════════════
/--
Hyperbolicity condition: a 1D system is hyperbolic when all characteristic
speeds are real and finite. For an Euler/gas-dynamics system, the three
characteristic speeds are:
λ₋ = u c_s, λ₀ = u, λ₊ = u + c_s
Hyperbolicity holds if c_s > 0 (positive, real sound speed). We check
soundSpd on both sides. If either side has c_s = 0 the system is parabolic
or degenerate at that state.
Returns `true` when both states pass the hyperbolicity check.
-/
def hyperbolicityGate (ev : ShockEvent) : Bool :=
ev.stateL.soundSpd.val > 0 && ev.stateR.soundSpd.val > 0
/--
Characteristic speeds for a given state: (λ₋, λ₀, λ₊).
Speeds are Q16_16 magnitudes; sign information is tracked externally.
-/
def characteristicSpeeds (s : FluidState) : Q16_16 × Q16_16 × Q16_16 :=
let lMinus := q_absdiff s.velocity s.soundSpd
let lZero := s.velocity
let lPlus := q_add s.velocity s.soundSpd
(lMinus, lZero, lPlus)
#eval characteristicSpeeds
{ density := ⟨65536⟩, velocity := ⟨65536⟩ -- u = 1 km/s
, pressure := ⟨65536⟩, energy := ⟨65536⟩
, soundSpd := ⟨21953⟩ } -- c_s ≈ 0.335 km/s (air)
-- expected: λ₋ ≈ 0.665, λ₀ ≈ 1.000, λ₊ ≈ 1.335 (all in per-km/s)
-- ═══════════════════════════════════════════════════════════════════
-- §4 RankineHugoniot Residual
-- ═══════════════════════════════════════════════════════════════════
/--
RankineHugoniot jump conditions for a 1D inviscid compressible flow.
The three conservation laws across a stationary frame shock at speed s are:
[ρ(u s)] = 0 (mass)
[ρu(us) + p] = 0 (momentum)
[ρe(us) + pu] = 0 (energy)
where [·] = (·)_R (·)_L.
We compute unsigned residuals ε_mass, ε_mom, ε_energy as proxy distances
in Q16_16 units. Exact enforcement would require field arithmetic (Real),
so these are *relative* residuals: (|ΔF|) / F_scale, with F_scale chosen
as the left-side flux magnitude.
A residual of 0 means exact balance. A residual > `ε_threshold` means the
jump fails the RH gate.
-/
structure RHResidual where
epsMass : Q16_16
epsMomentum : Q16_16
epsEnergy : Q16_16
deriving Repr, BEq, DecidableEq, Inhabited
/--
Compute the RankineHugoniot residual for a shock event.
Approximation note: mass flux proxy = ρ_L × (u_L s).
Momentum flux proxy = p_R p_L (dominant when u ~ s is small).
Energy proxy = |e_R e_L| relative to e_L.
These are structurally correct diagnostics, not exact SI simulations.
-/
def rankineHugoniotResidual (ev : ShockEvent) : RHResidual :=
let rhoL := ev.stateL.density
let rhoR := ev.stateR.density
let uL := ev.stateL.velocity
let uR := ev.stateR.velocity
let pL := ev.stateL.pressure
let pR := ev.stateR.pressure
let eL := ev.stateL.energy
let eR := ev.stateR.energy
let s := ev.frontSpeed
-- mass flux residual: |ρ_R(u_Rs) ρ_L(u_Ls)| / ρ_L
-- All intermediate products lifted to Nat to avoid UInt32 overflow.
let mFluxLN := toN (q_absdiff uL s)
let mFluxRN := toN (q_absdiff uR s)
let rhoLN := toN rhoL
let rhoRN := toN rhoR
let prodL := (rhoLN * mFluxLN) / 65536
let prodR := (rhoRN * mFluxRN) / 65536
let massDeltaN := if prodR ≥ prodL then prodR - prodL else prodL - prodR
let epsMN := if rhoLN > 0 then (massDeltaN * 65536) / rhoLN else massDeltaN
let epsM := ⟨(min epsMN 0xFFFFFFFF).toUInt32⟩
-- momentum residual: |p_R p_L| / p_L
let epsMom := if pL.val > 0 then q_div (q_absdiff pL pR) pL else q_absdiff pL pR
-- energy residual: |e_R e_L| / e_L
let epsEng := if eL.val > 0 then q_div (q_absdiff eL eR) eL else q_absdiff eL eR
{ epsMass := epsM, epsMomentum := epsMom, epsEnergy := epsEng }
#eval rankineHugoniotResidual
{ stateL := { density := ⟨65536⟩, velocity := ⟨131072⟩, pressure := ⟨65536⟩
, energy := ⟨65536⟩, soundSpd := ⟨21953⟩ }
, stateR := { density := ⟨104858⟩, velocity := ⟨81920⟩, pressure := ⟨104858⟩
, energy := ⟨104858⟩, soundSpd := ⟨25000⟩ }
, frontSpeed := ⟨65536⟩ }
-- ε_mass, ε_momentum, ε_energy all printed
-- ═══════════════════════════════════════════════════════════════════
-- §5 Entropy (Lax) Admissibility Condition
-- ═══════════════════════════════════════════════════════════════════
/--
Entropy admissibility (Lax entropy condition).
A compressive shock is admissible if the entropy *increases* across the front:
s(state_R) ≥ s(state_L)
For a polytropic gas with γ-law equation of state, entropy is monotone in
p/ρ^γ. We approximate this with the proxy:
entropy_proxy(state) = pressure / density
(Valid for γ = 1 surrogate; structurally captures the admissibility sign.)
A shock is admissible (second-law) iff entropy_R ≥ entropy_L.
-/
def entropyProxy (s : FluidState) : Q16_16 :=
if s.density.val > 0 then q_div s.pressure s.density else ⟨0⟩
/--
Returns true when the shock is entropy-admissible (ΔS ≥ 0).
-/
def entropyAdmissible (ev : ShockEvent) : Bool :=
(entropyProxy ev.stateR).val ≥ (entropyProxy ev.stateL).val
/--
Entropy gain across the shock: S_R S_L (in entropy-proxy units).
Zero for isentropic transitions; positive for physical shocks.
-/
def entropyGain (ev : ShockEvent) : Q16_16 :=
q_absdiff (entropyProxy ev.stateR) (entropyProxy ev.stateL)
#eval entropyAdmissible
{ stateL := { density := ⟨65536⟩, velocity := ⟨131072⟩, pressure := ⟨65536⟩
, energy := ⟨65536⟩, soundSpd := ⟨21953⟩ }
, stateR := { density := ⟨104858⟩, velocity := ⟨81920⟩, pressure := ⟨131072⟩
, energy := ⟨104858⟩, soundSpd := ⟨25000⟩ }
, frontSpeed := ⟨65536⟩ }
-- expected: true (pressure increased → entropy increased)
-- ═══════════════════════════════════════════════════════════════════
-- §6 Causal Front Constraint
-- ═══════════════════════════════════════════════════════════════════
/--
Causal front bound: the front speed s must remain within the sound-speed
envelope of both surrounding states. The envelope is:
s_min = min(u_L c_L, u_R c_R) (leftward fastest wave)
s_max = max(u_L + c_L, u_R + c_R) (rightward fastest wave)
A front with |s| > s_max violates causality (information would need to
propagate faster than the local sound speed).
We check the simpler necessary condition:
frontSpeed ≤ max(u_L + c_L, u_R + c_R)
and record the excess as a residual.
-/
def causalEnvelope (ev : ShockEvent) : Q16_16 :=
let sMaxL := q_add ev.stateL.velocity ev.stateL.soundSpd
let sMaxR := q_add ev.stateR.velocity ev.stateR.soundSpd
if sMaxL.val ≥ sMaxR.val then sMaxL else sMaxR
def causallyValid (ev : ShockEvent) : Bool :=
ev.frontSpeed.val ≤ (causalEnvelope ev).val
/--
Speed-excess residual: how far the front speed exceeds the causal envelope.
Zero for valid fronts.
-/
def causalExcess (ev : ShockEvent) : Q16_16 :=
let env := causalEnvelope ev
if ev.frontSpeed.val > env.val then ⟨ev.frontSpeed.val - env.val⟩ else ⟨0⟩
#eval causallyValid
{ stateL := { density := ⟨65536⟩, velocity := ⟨65536⟩, pressure := ⟨65536⟩
, energy := ⟨65536⟩, soundSpd := ⟨21953⟩ }
, stateR := { density := ⟨104858⟩, velocity := ⟨65536⟩, pressure := ⟨131072⟩
, energy := ⟨104858⟩, soundSpd := ⟨25000⟩ }
, frontSpeed := ⟨80000⟩ }
-- expected: true (frontSpeed < max(u+c) on both sides)
-- ═══════════════════════════════════════════════════════════════════
-- §7 Irreversibility Receipt
-- ═══════════════════════════════════════════════════════════════════
/--
Verdict enum for the shock gate.
-/
inductive ShockVerdict
| Admitted -- shock is hyperbolic, RH-close, entropy-admissible, causal
| RejectedRH -- fails RankineHugoniot balance (not a real shock surface)
| RejectedLax -- entropy-decreasing (inadmissible expansion shock)
| RejectedAcausal -- front speed exceeds causal envelope
| RejectedElliptic -- hyperbolicity check failed (degenerate state)
deriving Repr, BEq, DecidableEq, Inhabited
/--
Full diagnostic receipt for one shock event.
-/
structure ShockReceipt where
event : ShockEvent
hyperbolic : Bool
rhResidual : RHResidual
entropyGain : Q16_16
causalExcess : Q16_16
verdict : ShockVerdict
deriving Repr, Inhabited
/--
RH residual threshold: 5% in Q16_16 units = 0.05 × 65536 = 3277.
-/
def rhThreshold : Q16_16 := ⟨3277⟩
/--
Full shock gate evaluation: applies all four checks in order and returns a
typed `ShockReceipt`. The gate is a logical series circuit — one failed
check terminates further evaluation.
-/
def shockGate (ev : ShockEvent) : ShockReceipt :=
let hyp := hyperbolicityGate ev
if !hyp then
{ event := ev, hyperbolic := false
, rhResidual := { epsMass := ⟨0⟩, epsMomentum := ⟨0⟩, epsEnergy := ⟨0⟩ }
, entropyGain := ⟨0⟩, causalExcess := ⟨0⟩
, verdict := ShockVerdict.RejectedElliptic }
else
let rh := rankineHugoniotResidual ev
let rhFail := rh.epsMass.val > rhThreshold.val
|| rh.epsMomentum.val > rhThreshold.val
|| rh.epsEnergy.val > rhThreshold.val
if rhFail then
{ event := ev, hyperbolic := true, rhResidual := rh
, entropyGain := ⟨0⟩, causalExcess := ⟨0⟩
, verdict := ShockVerdict.RejectedRH }
else
let lax := entropyAdmissible ev
if !lax then
{ event := ev, hyperbolic := true, rhResidual := rh
, entropyGain := ⟨0⟩, causalExcess := ⟨0⟩
, verdict := ShockVerdict.RejectedLax }
else
let causal := causallyValid ev
if !causal then
{ event := ev, hyperbolic := true, rhResidual := rh
, entropyGain := entropyGain ev, causalExcess := causalExcess ev
, verdict := ShockVerdict.RejectedAcausal }
else
{ event := ev, hyperbolic := true, rhResidual := rh
, entropyGain := entropyGain ev, causalExcess := ⟨0⟩
, verdict := ShockVerdict.Admitted }
-- ═══════════════════════════════════════════════════════════════════
-- §8 Witnesses
-- ═══════════════════════════════════════════════════════════════════
/--
Canonical physical shock: weak compression (≈ 3% jump), entropy increase, subsonic front.
The states are chosen so that the RH proxy residuals fall below the 5% threshold:
ε_mass ~ 3% (density × velocity-shift imbalance)
ε_momentum ~ 3% (pressure jump / p_L)
ε_energy ~ 3% (energy jump / e_L)
All four gates pass: hyperbolic, RH-close, entropy-admissible, causal.
-/
def exampleShock : ShockEvent :=
{ stateL := { density := ⟨65536⟩ -- ρ_L = 1.000 (normalised)
, velocity := ⟨131072⟩ -- u_L = 2.000 km/s
, pressure := ⟨65536⟩ -- p_L = 1.000 bar
, energy := ⟨65536⟩ -- e_L = 1.000 MJ/kg
, soundSpd := ⟨21953⟩ } -- c_L ≈ 0.335 km/s (air-like)
, stateR := { density := ⟨67502⟩ -- ρ_R ≈ 1.030 (3% compression)
, velocity := ⟨127140⟩ -- u_R ≈ 1.940 km/s (slight slowdown)
, pressure := ⟨67502⟩ -- p_R ≈ 1.030 bar (3% pressure rise)
, energy := ⟨67502⟩ -- e_R ≈ 1.030 MJ/kg (3% energy rise)
, soundSpd := ⟨22283⟩ } -- c_R ≈ 0.340 km/s (slight increase)
, frontSpeed := ⟨65536⟩ } -- s = 1.0 km/s (≤ u_L + c_L = 2.335)
#eval shockGate exampleShock
-- expected: ShockVerdict.Admitted (all four gates pass)
/-- Degenerate state: zero sound speed → elliptic, rejected immediately. -/
def ellipticEvent : ShockEvent :=
{ stateL := { density := ⟨65536⟩, velocity := ⟨65536⟩, pressure := ⟨65536⟩
, energy := ⟨65536⟩, soundSpd := ⟨0⟩ } -- c = 0 → elliptic
, stateR := { density := ⟨65536⟩, velocity := ⟨65536⟩, pressure := ⟨65536⟩
, energy := ⟨65536⟩, soundSpd := ⟨21953⟩ }
, frontSpeed := ⟨65536⟩ }
#eval (shockGate ellipticEvent).verdict
-- expected: ShockVerdict.RejectedElliptic
/--
Entropy-decreasing front: small density jump (RH-close) but p_R < p_L
so entropy_proxy(R) = p_R/ρ_R < p_L/ρ_L = entropy_proxy(L).
Passes RH gate, fails Lax admissibility → RejectedLax.
-/
def expansionShock : ShockEvent :=
{ stateL := { density := ⟨65536⟩ -- ρ_L = 1.000
, velocity := ⟨131072⟩ -- u_L = 2.000 km/s
, pressure := ⟨65536⟩ -- p_L = 1.000 bar
, energy := ⟨65536⟩ -- e_L = 1.000 MJ/kg
, soundSpd := ⟨21953⟩ } -- c_L ≈ 0.335 km/s
, stateR := { density := ⟨65536⟩ -- ρ_R = 1.000 (same density — RH mass ε = 0)
, velocity := ⟨131072⟩ -- u_R = 2.000 (same — RH mom ε ≈ 0)
, pressure := ⟨63373⟩ -- p_R ≈ 0.967 bar (3% pressure DROP → entropy decrease)
, energy := ⟨65536⟩ -- e_R = same
, soundSpd := ⟨21953⟩ } -- c_R same
, frontSpeed := ⟨65536⟩ }
#eval (shockGate expansionShock).verdict
-- expected: ShockVerdict.RejectedLax (entropy_R < entropy_L: p_R/ρ_R < p_L/ρ_L)
/--
Superluminal (acausal) front: RH-close states (small jump) but frontSpeed >>
causal envelope (u + c_s on both sides ≈ 1.335 km/s = 87,489 Q16 units).
frontSpeed = 1,000,000 >> causal envelope → RejectedAcausal.
Entropy is admissible (p_R ≥ p_L), RH residuals are small → first three
gates pass; fourth (causal) fails.
-/
def acausalShock : ShockEvent :=
{ stateL := { density := ⟨65536⟩ -- ρ_L = 1.000
, velocity := ⟨65536⟩ -- u_L = 1.000 km/s
, pressure := ⟨65536⟩ -- p_L = 1.000
, energy := ⟨65536⟩ -- e_L = 1.000
, soundSpd := ⟨21953⟩ } -- c_L ≈ 0.335 km/s → u+c ≈ 87,489
, stateR := { density := ⟨65536⟩ -- same (RH ε → 0)
, velocity := ⟨65536⟩
, pressure := ⟨67502⟩ -- 3% pressure rise (entropy admissible)
, energy := ⟨65536⟩
, soundSpd := ⟨21953⟩ }
, frontSpeed := ⟨1000000⟩ } -- ~15 km/s — far exceeds causal envelope
#eval (shockGate acausalShock).verdict
-- expected: ShockVerdict.RejectedAcausal
-- ═══════════════════════════════════════════════════════════════════
-- §9 HCMMR Gate Bundle
-- ═══════════════════════════════════════════════════════════════════
/--
`A_shock(ev)` : the HCMMR shock admissibility gate.
Returns `true` iff the shock event is fully admitted (all four sub-gates pass).
This Boolean is the `A_shock` factor in the multiplicative eigenmass equation.
-/
def A_shock (ev : ShockEvent) : Bool :=
(shockGate ev).verdict == ShockVerdict.Admitted
/--
`A_shock` factor as Q16_16 weight for use in the eigenmass product chain.
Admitted = 1.0 = 65536; rejected = 0.
-/
def A_shock_weight (ev : ShockEvent) : Q16_16 :=
if A_shock ev then ⟨65536⟩ else ⟨0⟩
#eval A_shock_weight exampleShock -- expected: ⟨65536⟩ (admitted)
#eval A_shock_weight ellipticEvent -- expected: ⟨0⟩ (rejected)
end Semantics.HCMMR.Law20

View file

@ -0,0 +1,493 @@
/-
Law 21 — Thermal Boundary Gate
Formalises the HCMMR temperature-regime admissibility gate A_thermal.
Doctrine: temperature is a *gate variable*, not a free parameter. Two
hard boundaries bracket the physically accessible regime, and the CMB floor
anchors the observable cosmic background.
1. **Absolute zero boundary — 0 K = hard floor (not a state)**
T = 0 K is a asymptotic limit, never a reachable state. Any thermal
input claiming T ≤ 0 is inadmissible — an Underverse entry with a
"subliminal temperature" residual.
2. **CMB anchor — T_CMB ≈ 2.725 K**
The cosmic microwave background sets the coldest observable large-scale
thermal state in the present-epoch universe. Objects claimed below T_CMB
in an unshielded environment are flagged with a "subCMB" residual; they
are not rejected outright (local cooling below CMB is possible) but carry
a non-zero ambient-friction scar.
3. **Hagedorn / matter-phase ceiling — T_Hagedorn ≈ 10¹² K**
Above T_Hagedorn, hadronic matter undergoes a phase transition to a
quarkgluon plasma. The HCMMR boundary is set at 10¹² K. Objects
claiming T > 10¹² K are not rejected but are rerouted to a
"plasma phase" receipt — the Boltzmann/equipartition assumptions of
the thermal gate no longer apply and a separate plasma-regime gate is needed.
4. **Landauer threshold — ΔE ≥ k_B T ln 2 per bit erased**
Every irreversible computation has a minimum energy cost of k_B T ln 2.
The gate checks whether a proposed erasure event is above this threshold.
Below-threshold erasure claims are routed to the Underverse as
"sub-Landauer" violations.
5. **Thermal regime classification**
Based on T, objects are classified into: CryogenicDeep, CryogenicShallow,
Ambient, Hot, Plasma — each with distinct physics chart recommendations.
6. **Thermal receipt**
Every evaluation emits a typed `ThermalReceipt` recording the raw
temperature, the Landauer floor at that T, the regime class, and the
admissibility verdict.
Conventions:
PascalCase types, camelCase functions.
`structure` for domain concepts.
`def` needs `#eval` witness or `theorem`.
Q16_16 for all numeric fields.
Namespace: Semantics.HCMMR.Law21
Imports: Semantics.HCMMR.Core, Semantics.FixedPoint
-/
import Semantics.HCMMR.Core
import Semantics.FixedPoint
namespace Semantics.HCMMR.Law21
open Semantics.HCMMR.Core
open Semantics.FixedPoint (Q16_16)
-- ═══════════════════════════════════════════════════════════════════
-- §1 Thermal Constants
-- ═══════════════════════════════════════════════════════════════════
/--
Boltzmann constant: k_B = 1.380649 × 10⁻²³ J/K (exact SI 2019).
Stored as a rational value for Landauer floor computations.
Nat representation: 1380649 / (10^29). Not converted to Q16_16 directly
because thermal energies span 30+ orders of magnitude; instead we
compute k_B × T as a rational and convert the *ratio* to Q16_16 when needed.
-/
def boltzmann_num : Nat := 1380649 -- numerator × 10⁻²³
def boltzmann_den : Nat := 10000000 -- × 10^7 → effective 10⁻³⁰
/--
Cosmic microwave background temperature: T_CMB ≈ 2.72548 K (Fixsen 2009).
Stored in Q16_16 units where 1 K = 65536.
2.72548 × 65536 = 178,618 (rounded)
-/
def T_CMB : Q16_16 := ⟨178618⟩
/--
ln(2) in Q16_16: ln 2 ≈ 0.693147 × 65536 = 45,426.
Used in the Landauer threshold ΔE ≥ k_B T ln 2.
-/
def ln2_Q16 : Q16_16 := ⟨45426⟩
/--
Hagedorn temperature ceiling (HCMMR boundary): T_H = 10¹² K.
This exceeds Q16_16 range, so we store it as a Nat and only use it in
comparison logic (not arithmetic). Gate comparisons use integer temperature
values in units of millikelvin to avoid overflow in Q16_16.
In millikelvin: T_H = 10¹² K × 1000 mK/K = 10¹⁵ mK.
-/
def T_Hagedorn_K : Nat := 1000000000000 -- 10¹² K
/--
Absolute zero boundary: T_abs = 0 K. Any claimed T ≤ 0 is inadmissible.
Stored as Nat for comparison.
-/
def T_absZero_K : Nat := 0
-- ═══════════════════════════════════════════════════════════════════
-- §2 Temperature Input Model
-- ═══════════════════════════════════════════════════════════════════
/--
Thermal input: a claimed temperature and an energy budget for erasure.
- `temp_mK` : claimed temperature in millikelvin (Nat, avoids Q16_16 overflow)
- `energyBudget`: energy available for one-bit erasure, in units of 10⁻²³ J
(same scale as k_B so the Landauer comparison is unit-direct)
- `bitsToErase` : number of bits being erased (for multi-bit Landauer check)
-/
structure ThermalInput where
temp_mK : Nat -- millikelvin, avoids overflow
energyBudget : Nat -- in units of 10⁻²³ J per bit
bitsToErase : Nat
deriving Repr, BEq, DecidableEq, Inhabited
-- ═══════════════════════════════════════════════════════════════════
-- §3 Regime Classification
-- ═══════════════════════════════════════════════════════════════════
/--
Thermal regime classes based on temperature thresholds.
| Regime | Range | Physics chart |
|-----------------|-------------------|------------------------|
| SubZero | T ≤ 0 K | Inadmissible |
| CryogenicDeep | 0 < T < 1 K | Quantum degenerate |
| CryogenicShallow| 1 K ≤ T < 50 K | Liquid He / SuC regimes|
| Ambient | 50 K ≤ T < 1000 K | Classical stat-mech |
| Hot | 1000 K ≤ T < 10¹² K| Thermodynamic limit |
| Plasma | T ≥ 10¹² K | Hadronic phase break |
-/
inductive ThermalRegime
| SubZero -- T ≤ 0 K (inadmissible)
| CryogenicDeep -- 0 K < T < 1000 mK (1 K)
| CryogenicShallow -- 1000 mK ≤ T < 50000 mK (50 K)
| Ambient -- 50000 mK ≤ T < 1_000_000 mK (1000 K)
| Hot -- 1_000_000 mK ≤ T < 10¹² × 1000 mK
| Plasma -- T ≥ 10¹⁵ mK (10¹² K)
deriving Repr, BEq, DecidableEq, Inhabited
def classifyThermalRegime (inp : ThermalInput) : ThermalRegime :=
if inp.temp_mK = 0 then ThermalRegime.SubZero
else if inp.temp_mK < 1000 then ThermalRegime.CryogenicDeep
else if inp.temp_mK < 50000 then ThermalRegime.CryogenicShallow
else if inp.temp_mK < 1000000 then ThermalRegime.Ambient
else if inp.temp_mK < 1000000000000000 then ThermalRegime.Hot
else ThermalRegime.Plasma
#eval classifyThermalRegime { temp_mK := 2725, energyBudget := 0, bitsToErase := 0 }
-- expected: ThermalRegime.CryogenicShallow (2.725 K = 2725 mK)
#eval classifyThermalRegime { temp_mK := 293000, energyBudget := 0, bitsToErase := 0 }
-- expected: ThermalRegime.Ambient (293 K = 293000 mK, room temp)
-- ═══════════════════════════════════════════════════════════════════
-- §4 CMB Anchor Check
-- ═══════════════════════════════════════════════════════════════════
/--
T_CMB in millikelvin: 2725.48 mK (we use 2725 for integer comparison).
-/
def T_CMB_mK : Nat := 2725
/--
Returns `true` if the input temperature is at or above T_CMB.
Objects below T_CMB carry a non-zero ambient-friction scar but are not rejected.
-/
def aboveCMB (inp : ThermalInput) : Bool :=
inp.temp_mK ≥ T_CMB_mK
/--
Sub-CMB residual: how far below T_CMB the input is, in millikelvin.
Zero if at or above T_CMB.
-/
def subCMBresidual (inp : ThermalInput) : Nat :=
if inp.temp_mK < T_CMB_mK then T_CMB_mK - inp.temp_mK else 0
#eval aboveCMB { temp_mK := 300000, energyBudget := 0, bitsToErase := 0 }
-- expected: true (300 K >> 2.725 K)
#eval subCMBresidual { temp_mK := 1000, energyBudget := 0, bitsToErase := 0 }
-- expected: 1725 (mK below CMB)
-- ═══════════════════════════════════════════════════════════════════
-- §5 Landauer Threshold
-- ═══════════════════════════════════════════════════════════════════
/--
Landauer minimum energy per bit erased: ΔE_min = k_B × T × ln 2.
We compute this directly in units of 10⁻²³ J per bit:
k_B = 1380649 (where k_B_real = 1380649 × 10⁻²³⁻⁶ = 1.380649 × 10⁻²³ J/K)
T = inp.temp_mK / 1000 (convert mK → K)
ln2 = 6931 (ln2 × 10000, fixed-point 4-decimal approx)
Derivation (units of 10⁻²³ J):
k_B_real = 1.380649×10⁻²³ J/K = 1380649 × 10⁻²⁹ J/K
T_K = T_mK / 1000
ln2 = 6931 / 10000 (4-decimal fixed-point)
ΔE_min = k_B_real × T_K × ln2
= (1380649 × 10⁻²⁹) × (T_mK / 10³) × (6931 / 10⁴)
= 1380649 × T_mK × 6931 × 10⁻²⁹⁻³⁻⁴ J
= 1380649 × T_mK × 6931 × 10⁻³⁶ J
In units of 10⁻²³ J (divide by 10⁻²³):
= 1380649 × T_mK × 6931 / 10^(36-23)
= 1380649 × T_mK × 6931 / 10^13
Denominator 10^13 = 10^29 (k_B stored scale) / 10^23 (unit) × 10^3 (mK→K) × 10^4 (ln2 scaling).
At T=293 K: 1380649 × 293000 × 6931 / 10^13 ≈ 280 (in 10⁻²³ J units)
Actual k_B × 293 K × ln2 = 1.380649×10⁻²³ × 293 × 0.6931 ≈ 2.804×10⁻²¹ J = 280.4 × 10⁻²³ J ✓
-/
def landauerFloor (inp : ThermalInput) : Nat :=
-- ΔE_min in units of 10⁻²³ J per bit
-- = 1380649 × T_mK × 6931 / 10^13
(1380649 * inp.temp_mK * 6931) / 10000000000000
/--
Returns `true` if `energyBudget` ≥ Landauer floor per bit.
Both `energyBudget` (ThermalInput field) and `landauerFloor` are now in the
same units (10⁻²³ J), so the comparison is direct with no scaling factor.
-/
def landauerAdmissible (inp : ThermalInput) : Bool :=
inp.bitsToErase = 0 ||
inp.energyBudget ≥ landauerFloor inp
/--
Sub-Landauer deficit: how far the energy budget falls below the Landauer floor.
In units of 10⁻²³ J per bit. Zero if admissible.
-/
def landauerDeficit (inp : ThermalInput) : Nat :=
let floor := landauerFloor inp
if inp.energyBudget < floor then floor - inp.energyBudget else 0
#eval landauerFloor { temp_mK := 293000, energyBudget := 0, bitsToErase := 1 }
-- T = 293 K → ΔE_min = 1380649 × 293000 × 6931 / 10^13 ≈ 280
-- Actual: k_B × 293 K × ln2 ≈ 2.804 × 10⁻²¹ J = 280.4 × 10⁻²³ J ✓
#eval landauerAdmissible { temp_mK := 293000, energyBudget := 300, bitsToErase := 1 }
-- expected: true (300 × 10⁻²³ J > Landauer floor ~280 at 293 K)
#eval landauerAdmissible { temp_mK := 293000, energyBudget := 1, bitsToErase := 1 }
-- expected: false (1 × 10⁻²³ J << Landauer floor ~280 at 293 K)
-- ═══════════════════════════════════════════════════════════════════
-- §6 Full Thermal Gate
-- ═══════════════════════════════════════════════════════════════════
/--
Thermal admissibility verdict.
-/
inductive ThermalVerdict
| Admitted -- T in (0 K, 10¹² K), Landauer-satisfied
| RejectedSubZero -- T ≤ 0 K: absolute-zero violation
| RejectedPlasma -- T ≥ 10¹² K: Hagedorn phase break, reroute to plasma chart
| RejectedLandauer -- Erasure energy below Landauer floor
| AdmittedSubCMB -- Admitted but T < T_CMB: non-zero ambient scar attached
deriving Repr, BEq, DecidableEq, Inhabited
/--
Full thermal boundary receipt.
-/
structure ThermalReceipt where
input : ThermalInput
regime : ThermalRegime
subCMBresidual : Nat -- mK below CMB; 0 if above CMB
landauerFloor : Nat -- Landauer minimum in 10⁻²³ J per bit
landauerDeficit: Nat -- 0 if satisfied
verdict : ThermalVerdict
deriving Repr, Inhabited
/--
Thermal boundary gate: applies sub-zero check, Hagedorn ceiling, Landauer
threshold, and CMB scar tagging in order.
-/
def thermalGate (inp : ThermalInput) : ThermalReceipt :=
let regime := classifyThermalRegime inp
let subCMB := subCMBresidual inp
let floor := landauerFloor inp
let deficit := landauerDeficit inp
let verdict :=
if regime == ThermalRegime.SubZero then
ThermalVerdict.RejectedSubZero
else if regime == ThermalRegime.Plasma then
ThermalVerdict.RejectedPlasma
else if !landauerAdmissible inp then
ThermalVerdict.RejectedLandauer
else if subCMB > 0 then
ThermalVerdict.AdmittedSubCMB
else
ThermalVerdict.Admitted
{ input := inp, regime, subCMBresidual := subCMB
, landauerFloor := floor, landauerDeficit := deficit, verdict }
-- ═══════════════════════════════════════════════════════════════════
-- §6b ThermalSuperposition Receipt
--
-- Rather than hard-rejecting plasma or sub-Landauer inputs, the
-- superposition receipt carries three regime weights that describe
-- *which* physics chart the input inhabits:
--
-- ε_classical : Q16_16 — classical stat-mech weight (Boltzmann)
-- ε_quantum : Q16_16 — quantum / Landauer-constrained weight
-- ε_hadronic : Q16_16 — hadronic / quark-gluon plasma weight
--
-- The three weights sum to 65536 (= 1.0 in Q16_16).
-- Regime assignment rules:
-- SubZero → inadmissible: all weights zero, `inadmissible = true`
-- Admitted / AdmittedSubCMB → ε_classical = 65536, others = 0
-- RejectedLandauer → ε_quantum = 65536, others = 0
-- RejectedPlasma → ε_hadronic = 65536, others = 0
--
-- This replaces hard-reject semantics with a typed receipt that can be
-- combined with downstream gates (e.g. HyperEigenSpectrum, BoundaryEigenFire).
-- ═══════════════════════════════════════════════════════════════════
/--
Three-regime thermal superposition receipt.
All weight fields are Q16_16; their sum is 65536 for any admissible input,
and 0 for inadmissible (SubZero) inputs.
-/
structure ThermalSuperposition where
/-- Classical statistical mechanics weight (Boltzmann/equipartition valid). -/
ε_classical : Q16_16
/-- Quantum / Landauer-regime weight (quantum degenerate or sub-Landauer). -/
ε_quantum : Q16_16
/-- Hadronic / plasma-phase weight (Hagedorn transition exceeded). -/
ε_hadronic : Q16_16
/-- True iff the input is inadmissible (T ≤ 0 K). -/
inadmissible : Bool
deriving Repr, Inhabited
/--
Full thermal receipt extended with a ThermalSuperposition field.
-/
structure ThermalReceiptEx where
input : ThermalInput
regime : ThermalRegime
subCMBresidual : Nat -- mK below CMB; 0 if above CMB
landauerFloor : Nat -- Landauer minimum in 10⁻²³ J per bit
landauerDeficit: Nat -- 0 if satisfied
verdict : ThermalVerdict
superposition : ThermalSuperposition
deriving Repr, Inhabited
/--
Compute the `ThermalSuperposition` from a `ThermalVerdict`.
Weight assignment:
`Admitted` / `AdmittedSubCMB` → ε_classical = 65536 (full classical)
`RejectedLandauer` → ε_quantum = 65536 (quantum regime)
`RejectedPlasma` → ε_hadronic = 65536 (plasma regime)
`RejectedSubZero` → inadmissible = true, all weights 0
-/
def superpositionFromVerdict (v : ThermalVerdict) : ThermalSuperposition :=
match v with
| ThermalVerdict.Admitted | ThermalVerdict.AdmittedSubCMB =>
{ ε_classical := ⟨65536⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨0⟩
, inadmissible := false }
| ThermalVerdict.RejectedLandauer =>
{ ε_classical := ⟨0⟩, ε_quantum := ⟨65536⟩, ε_hadronic := ⟨0⟩
, inadmissible := false }
| ThermalVerdict.RejectedPlasma =>
{ ε_classical := ⟨0⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨65536⟩
, inadmissible := false }
| ThermalVerdict.RejectedSubZero =>
{ ε_classical := ⟨0⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨0⟩
, inadmissible := true }
/--
Theorem: weight sum is 65536 for all admissible inputs (not SubZero).
-/
theorem superposition_weight_sum (v : ThermalVerdict) (h : v ≠ ThermalVerdict.RejectedSubZero) :
let s := superpositionFromVerdict v
s.ε_classical.val + s.ε_quantum.val + s.ε_hadronic.val = 65536 := by
cases v <;> simp_all [superpositionFromVerdict]
/--
Extended thermal gate: combines the base `thermalGate` with a `ThermalSuperposition`
receipt, replacing hard-reject semantics with regime-typed weights.
-/
def thermalGateEx (inp : ThermalInput) : ThermalReceiptEx :=
let base := thermalGate inp
let super := superpositionFromVerdict base.verdict
{ input := base.input
, regime := base.regime
, subCMBresidual := base.subCMBresidual
, landauerFloor := base.landauerFloor
, landauerDeficit:= base.landauerDeficit
, verdict := base.verdict
, superposition := super }
-- ═══════════════════════════════════════════════════════════════════
-- §7 Witnesses
-- ═══════════════════════════════════════════════════════════════════
-- Room temperature (293 K) with adequate erasure budget → Admitted.
-- Landauer floor at 293 K ≈ 280 × 10⁻²³ J; budget=300 clears it.
#eval (thermalGate { temp_mK := 293000, energyBudget := 300, bitsToErase := 1 }).verdict
-- expected: ThermalVerdict.Admitted
-- Exactly at absolute zero → RejectedSubZero.
#eval (thermalGate { temp_mK := 0, energyBudget := 300, bitsToErase := 1 }).verdict
-- expected: ThermalVerdict.RejectedSubZero
-- Above Hagedorn ceiling → RejectedPlasma.
#eval (thermalGate { temp_mK := 1000000000000001, energyBudget := 300, bitsToErase := 1 }).verdict
-- expected: ThermalVerdict.RejectedPlasma
-- Sub-Landauer erasure at room temp → RejectedLandauer.
-- Budget = 1 × 10⁻²³ J << floor ≈ 280; correctly rejected.
#eval (thermalGate { temp_mK := 293000, energyBudget := 1, bitsToErase := 1 }).verdict
-- expected: ThermalVerdict.RejectedLandauer
-- 1 K (below CMB) with adequate budget, no erasure → AdmittedSubCMB (scar attached).
-- Landauer floor at 1 K ≈ 0.96 × 10⁻²³ J; bitsToErase=0 bypasses check.
#eval (thermalGate { temp_mK := 1000, energyBudget := 5, bitsToErase := 0 }).verdict
-- expected: ThermalVerdict.AdmittedSubCMB
-- Check the actual Landauer floor at room temperature (correctness witness).
#eval landauerFloor { temp_mK := 293000, energyBudget := 0, bitsToErase := 0 }
-- expected: 280 (1380649 × 293000 × 6931 / 10^13 ≈ 280.4 → truncated to 280)
-- CMB floor value stored as Q16_16 check.
#eval T_CMB
-- expected: ⟨178618⟩ (2.725 K × 65536)
-- ThermalSuperposition witnesses.
-- Admitted → full classical weight.
#eval (thermalGateEx { temp_mK := 293000, energyBudget := 300, bitsToErase := 1 }).superposition
-- expected: { ε_classical := ⟨65536⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨0⟩, inadmissible := false }
-- Plasma input → full hadronic weight (not a hard reject; receives plasma receipt).
#eval (thermalGateEx { temp_mK := 1000000000000001, energyBudget := 300, bitsToErase := 1 }).superposition
-- expected: { ε_classical := ⟨0⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨65536⟩, inadmissible := false }
-- Sub-Landauer input → full quantum weight (below Landauer floor; quantum regime receipt).
#eval (thermalGateEx { temp_mK := 293000, energyBudget := 1, bitsToErase := 1 }).superposition
-- expected: { ε_classical := ⟨0⟩, ε_quantum := ⟨65536⟩, ε_hadronic := ⟨0⟩, inadmissible := false }
-- SubZero input → inadmissible, all weights 0.
#eval (thermalGateEx { temp_mK := 0, energyBudget := 300, bitsToErase := 1 }).superposition
-- expected: { ε_classical := ⟨0⟩, ε_quantum := ⟨0⟩, ε_hadronic := ⟨0⟩, inadmissible := true }
-- ε_classical weight check directly from superpositionFromVerdict.
#eval (superpositionFromVerdict ThermalVerdict.Admitted).ε_classical
-- expected: ⟨65536⟩
-- ε_hadronic check for plasma verdict.
#eval (superpositionFromVerdict ThermalVerdict.RejectedPlasma).ε_hadronic
-- expected: ⟨65536⟩
-- ═══════════════════════════════════════════════════════════════════
-- §8 HCMMR Gate Bundle
-- ═══════════════════════════════════════════════════════════════════
/--
`A_thermal(inp)` : the HCMMR thermal boundary gate.
Returns `true` iff the thermal input is admitted (not sub-zero, not plasma,
Landauer-satisfied — SubCMB counts as admitted with scar).
-/
def A_thermal (inp : ThermalInput) : Bool :=
let v := (thermalGate inp).verdict
v == ThermalVerdict.Admitted || v == ThermalVerdict.AdmittedSubCMB
/--
`A_thermal` factor as Q16_16 weight.
Admitted = 65536; rejected = 0.
-/
def A_thermal_weight (inp : ThermalInput) : Q16_16 :=
if A_thermal inp then ⟨65536⟩ else ⟨0⟩
#eval A_thermal_weight { temp_mK := 293000, energyBudget := 300, bitsToErase := 1 }
-- expected: ⟨65536⟩ (room-temp, admitted)
#eval A_thermal_weight { temp_mK := 0, energyBudget := 300, bitsToErase := 1 }
-- expected: ⟨0⟩ (absolute-zero floor, rejected)
end Semantics.HCMMR.Law21

View file

@ -0,0 +1,349 @@
# HCMMR Operadic Meta-Calculus — v0.2 Roadmap & Ontology
**Status:** Canonical frozen-core from ChatGPT conversation, pending formal Lean unification.
**Target:** `HCMMR/` directory under `Semantics/` — Laws and Kernels subdirectories stubbed, zero populated files.
---
## 1. Ontology — The Fundamental Shift
| Old paradigm | New paradigm |
|---|---|
| "impossible = nonexistent" | "impossible = failed a specific gate with typed diagnostic receipt" |
| A failed equation is discarded. | A failed equation is decomposed, residualed, rerouted, and receipted. |
| Failure is one monolithic event. | Failure is a typed multi-gate event with per-gate residuals. |
**Core doctrine:**
> The object is what survives the transforms. Its eigenmass is how strongly it survives. Its Underverse shadow is what survives as failure.
**Key distinction:** *failure of a claim ≠ destruction of the object*. A failed gate collapses that branch's admitted positive-ladder eigenmass, but the object persists as:
- residual shadow (Underverse entry)
- alternate typed geometry (e.g. $L^n$ gate instead of $L^2$)
- real-valued closure (where integer closure failed)
- typed diagnostic receipt
- loopback seed (re-expansion from 0D horizon)
---
## 2. Processing Flow
```
Entry: Object X enters the 16D transform stack
Extraction: C^total(X) u = λ u identifies dominant structural stability modes
Gate Evaluation: Object passes serially through multiplicative gate stack:
A → I → χ → R → Ω_K → Π
Result:
M⁺(X) : Admitted positive-ladder eigenmass
M⁻(X) : Residual / Underverse eigenmass
M±(X) = M⁺(X) M⁻(X) : Total signed stability
```
Each gate is a **logical series circuit**. If any gate reaches zero, the entire positive-ladder eigenmass branch collapses. The product form is essential because no amount of structural stability can compensate for a missing receipt, broken chirality, or failed admissibility.
---
## 3. Canonical Equation
$$
M_{\pm}(X) =
\frac{\lambda_1^+ \cdot A^+ \cdot I^+ \cdot \chi^+ \cdot R^+ \cdot \Omega_K^+ \cdot \Pi^+}
{1 + \varepsilon^+}
\;-\;
\frac{\lambda_1^- \cdot A^- \cdot I^- \cdot \chi^- \cdot R^- \cdot \Omega_K^- \cdot \Pi^-}
{1 + \varepsilon^-}
$$
### Gate Table
| Symbol | Gate | Role | Zero-failure consequence |
|---|---|---|---|
| $\lambda_1$ | Spectral Gate | Dominant stable eigenmode from $C_X^{total}$ | No dominant direction; object is noise |
| $A$ | Admissibility Gate | Typed entry/format/domain legality | Object rejected from that domain |
| $I$ | Invariant Gate | Conservation of declared invariants across transforms | Drift detected; no lawful preservation |
| $\chi$ | Chirality Gate | Orientation/handedness coherence | Ambiguous orientation; braid aliasing |
| $R$ | Receipt Gate | Continuity of CMMR/HCMMR receipt chain | Untraceable state; proof chain broken |
| $\Omega_K$ | Constant Calibration Gate | Calibration against $c$, $\hbar$, $G$, $k_B$, $\alpha$, $\pi$, $\tau$, $\varphi$, $e$ | No dimensional anchoring |
| $\Pi$ | Projection/Loopback Gate | Survival through dimensional gear reduction and 0D→16D permeability | Projection collapses irreversibly |
| $\varepsilon$ | Residual Friction | Typed scar burden from gate mismatches | Denominator grows, perceived stability decays |
**Additive is weaker:** in additive form, high $\lambda_1$ could compensate for $R=0$. Multiplicative prevents this — every gate must carry nonzero weight.
---
## 4. The Residual Law
### Formal Law
$$
\varepsilon_{L^2}(n) = d(G_n, G_{L^2})
$$
The Euclidean residual is the *distance* between the object's native geometry $G_n$ and the Euclidean $L^2$ metric gate. This is the abstract, defensible form.
### Demo Curve (visual metaphor only — not a physical law)
$$
\varepsilon_{\text{demo}}(n) = |n - 2| \cdot e^{\alpha n}
$$
Captures the qualitative shape: zero at $n=2$, growing mismatch as $n$ departs. The coefficient $\alpha$ is a tunable display parameter, not a derived physical constant.
### Total Residual Composition
$$
\varepsilon_{\text{total}} = \varepsilon_{L^2} + \varepsilon_{\mathbb{Z}} + \varepsilon_{\chi} + \varepsilon_{\text{projection}} + \varepsilon_{\text{S3C}} + \varepsilon_{\text{underverse}} + \varepsilon_{\text{gauge}} + \varepsilon_{\text{Lorentz}} + \varepsilon_{\text{wave}} + \cdots
$$
Total residual is additive across gate dimensions: metric mismatch, integer closure gap, chirality ambiguity, projection loss, shell/underverse friction, gauge non-closure, coupling mismatch, and wave distortion.
---
## 5. The Law Stack
### Laws 1418 (v0.2 Core Recovery Gates)
| Law | Name | What it recovers | Gate name |
|---|---|---|---|
| 14 | Motion Recovery | $F=ma$, $p=mv$, $E=\frac12 mv^2$, $\delta S=0$, Lagrange-Euler equations | $A_{\text{motion}}$ |
| 15 | Field Recovery | Maxwell's equations, gauge invariance, vacuum waves, charge coupling | $A_{\text{field}}$ |
| 15K | Kähler Compatibility | Smooth-field gearbox: $\omega(X,Y)=g(JX,Y)$, $d\omega=0$, $J^2=-I$. Verifies that phase $J$, metric $g$, and symplectic flow $\omega$ form a compatible projection layer between 16D torsion and 4D $A_\mu/F_{\mu\nu}$. | `kahler_gate` |
| 15A | Gauge Invariance | $F_{\mu\nu}$ unchanged under $A_\mu \to A_\mu + \partial_\mu\Lambda$ | `gauge_gate` |
| 15B | Maxwell Equations | Homogeneous ($F=dA$) + Sourced ($\partial_\mu F^{\mu\nu}=J^\nu$) | `maxwell_gate` |
| 15C | Vacuum Wave Propagation | $\Box A^\nu=0$, transversality, causal speed $c$ | `wave_gate` |
| 15D | Charge/Current Coupling | $f^\mu=F^{\mu\nu}J_\nu$, $\mathbf{F}=q(\mathbf{E}+\mathbf{v}\times\mathbf{B})$ | `lorentz_gate` |
| 15E | Signal Detection | SNR-based pattern matching: narrowband spikes, broadband rises, Doppler drift, periodic pulsars, flicker transients. Detects whether a projected EM field contains a candidate signal above the noise floor. | `signal_gate` |
| 16 | Entropy/Heat Leak | Landauer limit $\Delta E \ge k_B T \ln 2$, Underverse as heat sink | $A_{\text{thermo}}$ |
| 17 | Observer/Measurement | Wavefunction collapse as typed gate event | $A_{\text{obs}}$ |
| 18 | Scale/Constant Anchoring | Recover $c$, $\hbar$, $G$ as limiting calibration constants; test dimensionless outputs ($\alpha$, mass ratios) | $A_{\text{const}}$ |
### Laws 1921 (Substrate & Boundary Gates — added during torsion/horizon work)
| Law | Name | What it enforces | Gate name |
|---|---|---|---|
| 19 | Ordered Field Gate | Scalar gates live in ordered field with positive cone; sign, thresholding, admissibility are lawful | $A_{\text{order}}$ |
| 20 | Shockwave/Front Gate | Discontinuity modeling, causal fronts, irreversible jumps, hyperbolicity conditions | $A_{\text{shock}}$ |
| 21 | Thermal Boundary Gate | $0\,\text{K}$ = boundary (not state), $10^{12}\,\text{K}$ = matter-phase regime break | $A_{\text{thermal}}$ |
**Law 14 pass condition:** $\varepsilon_{\text{motion}} = \|m\ddot{x} - F\| \to 0$ in the Newtonian limit. The 16D manifold must gear-reduce to classical mechanics when residuals are small, speeds are low, and fields are weak.
**Law 15K — Kähler Compatibility Gate:** A projected field manifold may claim smooth field relevance only if its complex/phase structure $J$, metric $g$, and symplectic form $\omega$ satisfy Kähler compatibility with bounded residual:
$$\varepsilon_{\text{K}} = \|\omega(X,Y) - g(JX,Y)\| + \|d\omega\| + \|J^2 + I\|$$
$A_{\text{Kähler}} = 1 \iff \varepsilon_{\text{K}} \le \tau_{\text{K}}$. This sits as a pre-gate before Maxwell recovery: the 16D torsion/winding/chirality state reduces via $\Pi_{16\to4}: T_{16} \Rightarrow (M,J,g,\omega) \Rightarrow A_\mu, F_{\mu\nu}$. When the Kähler manifold is fractally folded (rough geometry), $\varepsilon_{\text{K}} > 0$ — the smooth field claim is held or rejected, and the object routes to shock/fractal residual handling.
**Law 15D pass condition:** the projected field strength $F_{\mu\nu}$ must correctly grip the projected source current $J^\nu$, producing Lorentz force and conserving stress-energy: $\partial_\nu (T^{\mu\nu}_{\text{matter}} + T^{\mu\nu}_{\text{EM}}) = 0$.
**Law 18 scope:** HCMMR does not predict $c$, $\hbar$, $G$ as raw numerical values (these are dimensionful, unit-dependent). It recovers their *roles* as limiting calibration constants and targets *dimensionless* outputs: $\alpha$, mass ratios, coupling ratios, CMB anisotropy ratios.
---
## 6. RecamánFAMM Kernel Layer
### Recamán's Signed-Step Reflex → HCMMR Mapping
Classical Recamán:
$$
a_0 = 0,\qquad
a_n = \begin{cases}
a_{n-1} - n, & \text{if } a_{n-1}-n > 0 \text{ and unused} \\
a_{n-1} + n, & \text{otherwise}
\end{cases}
$$
This is isomorphic to HCMMR gate logic:
| Recamán feature | HCMMR interpretation |
|---|---|
| step size $n$ | gear tooth / action quantum / transition impulse |
| move backward ($a_{n-1}-n$) | Underverse / negative-dimensional attempt |
| move forward ($a_{n-1}+n$) | positive-ladder projection |
| `unused` constraint | no duplicate receipt / no collision on visited-set |
| failed backward move → forward reflection | gate rejection → reroute |
| arc drawing | braid/rope crossing history |
| repeated near-crossings | coupling/frustration scars |
### FAMM Scar & Frustration Memory
FAMM biases the step via memory of prior frustration:
$$
\Delta_n^F = n \cdot g_{\text{field}}(p_n) \cdot \Phi_{\text{FAMM}}(p_n),\qquad
\Phi_{\text{FAMM}} = \exp[-\gamma(\Sigma^2 + I_{\text{lock}} + \Delta\phi)]
$$
Where:
- $\Sigma^2$ = accumulated scar/frustration energy
- $I_{\text{lock}}$ = interference or lock-in penalty
- $\Delta\phi$ = phase mismatch
- $\gamma$ = damping/sensitivity coefficient
High FAMM frustration suppresses step magnitude. Low frustration permits aggressive exploration.
### Prime Exponent Caching
Factor step index $n = \prod p^{v_p(n)}$, compose from cached prime-step receipts:
$$
\Delta_n^F = g_{\text{field}}(p_n) \cdot \prod_{p \mid n} \left(\Delta_p^F\right)^{v_p(n)}
$$
Composites are derived, not recomputed. A `PrimeGearCache` stores per-prime: delta, field response, FAMM scar, braid crossing receipt, chirality receipt, residual, CMMR root.
### Circle-Packing Interpretation
Each Recamán step is a semicircle:
$$
x_n(\theta) = m_n + r_n \cos\theta,\quad
y_n(\theta) = s_n r_n \sin\theta
$$
where $m_n = \frac{a_{n-1}+a_n}{2}$, $r_n = \frac{n}{2}$, $s_n \in \{+1,-1\}$, $\theta \in [0,\pi]$.
**Cheap trig shortcuts:**
- Arc length: $L_n = \pi r_n = \pi n/2$, cumulative $L_{\le N} = \pi N(N+1)/4$
- Curvature: $\kappa_n = 1/r_n = 2/n$
- Circle intersection: $d_{ij} = |m_i - m_j|$ vs. $r_i + r_j$ (cheap sign check)
- Transversality: $\mathbf{E} \cdot k$, $\mathbf{B} \cdot k$, $\mathbf{E} \cdot \mathbf{B}$ residuals compute directly from arc geometry
---
## 7. FLT Diagnostic — Dual-Gate Reroute
Fermat's Last Theorem is interpreted through three independent gates:
| Case | $L^2$ Euclidean Gate | $L^n$ Metric Gate | $\mathbb{Z}^+$ Integer Gate |
|---|---|---|---|
| $n=1$ | Reject $(\varepsilon_{L^2}>0)$ | Admit $(\varepsilon_{L^1}=0)$ | Admit $(\varepsilon_{\mathbb{Z}}=0)$ |
| $n=2$ | Admit $(\varepsilon_{L^2}=0)$ | Admit $(\varepsilon_{L^2}=0)$ | Admit for Pythagorean triples |
| $n>2$ | Reject $(\varepsilon_{L^2}>0)$ | Admit $(\varepsilon_{L^n}=0)$ | Reject by FLT $(\varepsilon_{\mathbb{Z}}>0)$ |
The equation $a^n+b^n=c^n$ for $n>2$ is: metric-valid (in $L^n$), Euclidean-invalid, integer-invalid. The receipt carries all three gate outcomes. No branch is discarded — failed branches become typed Underverse entries.
**Canonical receipt for $n=3$:**
```text
HCMMRReceipt:
symbolic_status: valid_form = true
metric_gate_L2: admitted=false, ε_L2 > 0
metric_gate_L3: admitted=true, ε_L3 = 0
integer_gate_Z: admitted=false, ε_Z > 0 (FLT)
final_status:
valid_as: L3 metric object
invalid_as: Euclidean right-triangle, positive-integer Fermat closure
```
---
## 8. Implementation Map
### Law → Lean File Mapping
| Law | Target file | Bridged from / depends on |
|---|---|---|
| 14 — Motion Recovery | `HCMMR/Laws/Law14_Motion.lean` | `HamiltonianVerification.lean`, `PhysicsLagrangian.lean`, `UniversalCoupling.lean` |
| 15 — Field Recovery (master) | `HCMMR/Laws/Law15_Field.lean` | `SigmaGate.lean` (gating pattern), `ReceiptCore.lean` |
| 15A — Gauge Invariance | `HCMMR/Laws/Law15A_Gauge.lean` | imports $A_\mu$, $F_{\mu\nu}$ definitions from Law15 |
| 15B — Maxwell Equations | `HCMMR/Laws/Law15B_Maxwell.lean` | depends on 15A (homogeneous auto from $F=dA$, sourced needs action) |
| 15C — Vacuum Wave | `HCMMR/Laws/Law15C_Wave.lean` | depends on 15B sourced-free limit |
| 15D — Charge Coupling | `HCMMR/Laws/Law15D_Coupling.lean` | `UniversalCoupling.lean` ($J_n$ pattern), `ElectrostaticsMetaprobe.lean` |
| 16 — Entropy/Heat Leak | `HCMMR/Laws/Law16_Thermo.lean` | `ThermodynamicSort.lean` (Landauer partition), `EntropyMeasures.lean` |
| 17 — Observer/Measurement | `HCMMR/Laws/Law17_Observer.lean` | `ReceiptCore.lean` (authority states), `PIST.lean` (state machine) |
| 18 — Constant Anchoring | `HCMMR/Laws/Law18_Constants.lean` | `SIConstants.lean` (exact SI constants), `fundamental_math_verifier.py` |
| 19 — Ordered Field | `HCMMR/Laws/Law19_OrderedField.lean` | Mathlib `Algebra/Order/` imports |
| 20 — Shockwave/Front | `HCMMR/Laws/Law20_Shock.lean` | `PIST.lean` (discrete transitions) |
| 21 — Thermal Boundary | `HCMMR/Laws/Law21_ThermalBoundary.lean` | `SIConstants.lean`, $k_B$, $T_{\text{CMB}}$ |
| RecamánFAMM Kernel | `HCMMR/Kernels/RecamanFAMM.lean` | `FAMM.lean`, `PIST.lean`, `ReceiptCore.lean` |
### Existing Codebase Assets (scattered across 704+ files)
| Module | File | What it provides to HCMMR |
|---|---|---|
| FAMM | `FAMM.lean` | Delay-line memory, delay mass, frustration gates — kernel substrate |
| Sigma Gate | `SigmaGate.lean` | Conformal confidence gating, admission with fixed-point scores |
| Universal Coupling | `UniversalCoupling.lean` | $J(n)$ scoring kernel, domain-agnostic trajectory propagation |
| Folded Point Manifold | `Core/FoldedPointManifold.lean` | `GateOutcome`, `FoldDecision`, `LoopbackDecision`, permeability witness |
| Underverse Zero Layer | `Core/UnderverseZeroLayer.lean` | Neutral closure accounting, charge charts, replay receipts |
| PIST | `PIST.lean` | Lyapunov state machine, shell coordinates, mass, mirror, resonance |
| Hamiltonian Verification | `HamiltonianVerification.lean` | Newtonian limit recovery, dimensional consistency proofs |
| Physics Lagrangian | `PhysicsLagrangian.lean` | Lagrangian state, kinetic proxy, transport weight, linear advance |
| Thermodynamic Sort | `ThermodynamicSort.lean` | Landauer threshold partitions, thermo bind |
| SI Constants | `SIConstants.lean` | Exact SI 2019 defining constants, derived constants, CODATA values |
| Receipt Core | `ReceiptCore.lean` | Receipt kinds, receipt structure, validation/authority logic |
---
## 9. v0.1 → v0.2 Gap Analysis
### What v0.1 has (from the chat, frozen conceptually)
- **Ontology:** the "impossible ≠ nonexistent" doctrine, gate decomposition, typed diagnostics
- **Canonical equation:** multiplicative eigenmass equation with seven-factor gate stack
- **Residual law:** formal distance abstract, demo curve as visual metaphor
- **FLT diagnostic:** three-gate reroute table
- **Law 14:** motion recovery conceptually specified
- **Law 15A15D:** field recovery conceptually specified
- **Recamán-FAMM:** kernel layer drafted
- **Torsion-light horizon:** "add another 9" model via $E=\gamma mc^2$
### What the codebase already has (scattered, un-unified)
- **Gate infrastructure:** `SigmaGate.lean`, `FoldedPointManifold.lean`, `ReceiptCore.lean` define gate-like admission structures but are not unified into the HCMMR multiplicative chain.
- **Eigenmass:** `FAMM.lean` defines delay mass but not Meta Semantic Eigenmass.
- **Underverse accounting:** `UnderverseZeroLayer.lean` defines charge closure but not the signed dimensional ladder or the residual heat sink.
- **Motion:**
- `HamiltonianVerification.lean` has dimensional consistency proofs for kinetic energy and regularized potentials.
- `PhysicsLagrangian.lean` defines Lagrangian state with kinetic proxy and linear advance.
- `UniversalCoupling.lean` defines $J_n$ trajectory scoring.
- **Missing:** the gear-reduction proof connecting 16D state → Newtonian limit.
- **Fields:**
- `ElectrostaticsMetaprobe.lean`, `EntropyMeasures.lean` exist but are not wired to the field recovery gate.
- **Missing:** $F_{\mu\nu}$ projection from 16D torsion/winding state; gauge invariance residual; Maxwell equation residuals.
- **Thermodynamics:**
- `ThermodynamicSort.lean` defines Landauer thresholds.
- **Missing:** entropy cost of gate failure, Underverse as heat sink, Landauer minimum per residual emission.
- **Constants:**
- `SIConstants.lean` provides exact SI constants.
- **Missing:** $\Omega_K$ calibration gate wiring constants into eigenmass; dimensionless output tests.
- **Observer:**
- `PIST.lean` defines discrete state machine transitions.
- **Missing:** measurement/collapse modeled as gate event.
- **Recamán-FAMM:**
- `PIST.lean` defines coordinate/shell/mass structure.
- `FAMM.lean` defines frustration memory.
- **Missing:** the unified signed-step kernel with prime caching and circle-packing geometry.
### The unification task for v0.2
The codebase's 704 files contain nearly all the pieces — gating infrastructure, fixed-point scoring, receipt types, thermodynamic thresholds, SI constants, Lagrangian mechanics, dimensional consistency proofs. The v0.2 gap is not *invention* of new math but **routing**: wiring existing structures into the unified HCMMR operator chain and proving the gear-reduction lemmas that show classical physics emerges as the low-residual limit.
---
## 10. Guardrails — What HCMMR Is NOT
| Is NOT | Is |
|---|---|
| A theory of everything. | A ruleset for preserving distinctions when objects fail gates. |
| Claiming to predict physical constants numerically. | Claiming roles of $c$, $\hbar$, $G$ as limiting calibration constants; targeting dimensionless ratios. |
| Claiming all failed objects are physically realizable. | Claiming failure produces typed diagnostic receipts that may be useful for alternate routing. |
| A destructive filter that throws away failed objects. | A diagnostic machine that decomposes failure into per-gate residuals with traceable receipts. |
| A replacement for domain-specific physics modeling. | A meta-layer that asks: "Can this object be lawfully projected from 16D into this domain gate?" |
| Claiming superluminal or sub-zero phenomena. | Respecting $0\,\text{K}$ as thermal boundary and $c$ as causal horizon, asymptotically approachable, never crossable. |
### The load-bearing defense
> *"I am not claiming all failed mathematical objects are physically realizable. I am claiming that 'failure' should be decomposed. A symbolic object can fail Euclidean geometry, pass an $L^p$ metric gate, fail integer closure, pass real-valued closure, and still carry a useful residual receipt. HCMMR is a ruleset for preserving those distinctions."*
---
## Document References
- **Chat source:** `ChatGPT-Pythagorean_Theorem_and_Beyond.json` (conversation dated 2026-05-10/11)
- **Existing gate infrastructure:** `SigmaGate.lean`, `FoldedPointManifold.lean`, `ReceiptCore.lean`
- **Eigenmass / FAMM:** `FAMM.lean`
- **Underverse accounting:** `Core/UnderverseZeroLayer.lean`
- **Motion/Lagrangian:** `HamiltonianVerification.lean`, `PhysicsLagrangian.lean`, `UniversalCoupling.lean`
- **Thermodynamics:** `ThermodynamicSort.lean`
- **Constants:** `SIConstants.lean`
- **State machine:** `PIST.lean`

41
CITATION.cff Normal file
View file

@ -0,0 +1,41 @@
cff-version: 1.2.0
message: "If you use Research Stack, OTOM, Rainbow Raccoon Compiler, or the associated formal/compression artifacts, please cite this repository."
type: software
title: "Research Stack (OTOM)"
abstract: >-
Research Stack is a formal-methods and compression research repository for
integer-routed symbolic systems, Omindirection logogram atoms, the Rainbow
Raccoon Compiler admission gate, Lean-backed semantics, and associated
documentation, infrastructure, and experimental adapters.
authors:
- family-names: "Schneider"
given-names: "Brandon"
alias: "allaunthefox"
- name: "Research Stack Contributors"
repository-code: "https://github.com/allaunthefox/Research-Stack"
url: "https://github.com/allaunthefox/Research-Stack"
date-released: 2026-05-08
license: Apache-2.0
keywords:
- formal-verification
- lean4
- compression
- symbolic-systems
- omindirection
- rainbow-raccoon-compiler
- hutter-prize
- fpga
- manifolds
- reproducible-research
preferred-citation:
type: software
title: "Research Stack (OTOM)"
authors:
- family-names: "Schneider"
given-names: "Brandon"
alias: "allaunthefox"
- name: "Research Stack Contributors"
repository-code: "https://github.com/allaunthefox/Research-Stack"
url: "https://github.com/allaunthefox/Research-Stack"
date-released: 2026-05-08
license: Apache-2.0

14
NOTICE Normal file
View file

@ -0,0 +1,14 @@
Research Stack (OTOM)
Copyright 2026 Brandon Schneider and Research Stack Contributors
This product includes software and documentation developed for the Research
Stack / OTOM project.
Unless a file, directory, vendored dependency, generated artifact, dataset, or
third-party subtree states a different license, repository source code and
documentation are made available under the Apache License, Version 2.0.
Third-party components, copied datasets, generated corpora, notebooks, papers,
models, and external examples may carry their own licenses or terms. Their
upstream notices remain authoritative for those components. This NOTICE file
does not relicense third-party material.