Physics sandbox (Gnosis Lean)

Parent README: ../README.md
Formal index: ../FORMAL_LEDGER.md
Randomness / information adjacency: ./RANDOMNESS.md
Heritage vs Init-only minimal split: ./PHYSICS_SANDBOX_HERITAGE_VS_MINIMAL.md

This document maps the layered Mathlib-backed “physics sandbox” in open-source/gnosis/lean/Lean/ and records what is proved versus what remains narrative or future work.

For the separate discrete seismic stress toy (Init/ℕ sketches + executable TS, not continuum wave physics), see SEISMIC_STRESS_TOY.md.

For the same discrete mass / normalization story with no Mathlib (only [Init], Nat on [Fin n]), see DiscreteFiniteInfo.lean and MATH_SANDBOX.md — the Mathlib thermo rows below are the analysis-backed lane.

Entry point

PhysicsSandbox.lean — import-only hub; build with lake build PhysicsSandbox (see lakefile.lean).

Layers and Mathlib dependencies

Layer	Lean module	Role	Gaps
Classical	`ClassicalSandbox.lean`	Constant-velocity and linear `ẋ = a·x` ODEs via Picard–Lindelöf	Not Hamiltonian / symplectic geometry
Thermo / info	`LandauerInformationPhysics.lean`	`k_B T ln 2` scale	Continuum thermodynamics, devices
Thermo / Shannon	`ThermoInformationBridge.lean`	Fair `Fin 2` Shannon = `ln 2`; `shannonEntropyOnFinset` + support equality; uniform on a `Finset` / Fintype gives `log` cardinality; independent joint `prodPMF`; `shannonEntropy_prod_independent`; marginals `marginalX`/`marginalY`, conditional entropies both ways, chain rules `chain_rule_joint_add_marginalX`/`chain_rule_joint_add_marginalY`, `mutualInformation_marginals` + `mutualInformation_eq_sub_X`/`_Y`; `mutualInformation_eq_klFun_sum` / `mutualInformation_nonneg` / `shannonEntropy_joint_le_add_marginals` (finite PMF, via `InformationTheory.klFun`); doc links `InformationTheory.klDiv_eq_integral_klFun` for the Mathlib KL integral; `conditionalEntropy_*_prodPMF`; `mutualInformation_prod_independent`; product-uniform `shannonEntropy_prod_uniform`; Landauer energy factor match	Differential entropy, infinite countable carriers, continuous reference measures (this file stays finite / discrete)
Thermo / KL core (hub)	`ThermoFiniteKLCore.lean`	Convenience import: [`ThermoInformationBridge`] + [`ThermoPMFKLFintype`] (pulls [`ThermoPMFKLStructuralErrorgleton`]); nonnegative-real `pmfOfNonnegReal`, finite `klDiv.toReal` as singleton-mass / ratio sums	Same gaps as the bundled modules
Thermo / singleton RN	`ThermoPMFKLStructuralErrorgleton.lean`	`(μ.rnDeriv ν z) * ν {z} = μ {z}` and `toReal` ratio; [`rnDeriv_mul_measure_singleton`] applies Mathlib `Measure.setLIntegral_rnDeriv'` (Radon–Nikodym decomposition import — not redundant)	Non-discrete RN story beyond singleton mass
Thermo / PMF bridge	`ThermoPMFKLBridge.lean`	[`jointPMFOfReal`] / [`prodMarginalPMFOfReal`] as `PMF (ι × κ)` from nonnegative real masses; [`klDiv_toReal_eq_mutualInformation`]	Continuous carriers, non-`PMF` reference measures
Thermo / uniform KL	`ThermoUniformKLBridge.lean`	[`massPMFOfReal`] vs [`uniformPMF`]; [`klDiv_uniform_toReal_eq`] (`log	ι
BH information	`BlackHoleInformationSketch.lean`	Coarse maps vs `Equiv`	QFT, Hawking flux, AdS/CFT
Quantum (algebra)	`QuantumInfoSandbox.lean`	CHSH / Tsirelson via `Mathlib.Algebra.Star.CHSH`; permutations	Hilbert-space models, devices
Topological Friction	`TopologicalFriction.lean`	Maps Charisma Toy Model fear/resistance collisions to Landauer heat dissipation (`k_B T ln 2` penalty) and Zero-Friction traversals.	Dynamic heat flow models
Topological Exclusion	`TopologicalExclusion.lean`	Formalizes the Pauli Exclusion Principle for the mesh; Fermionic states enforce Mutex locks (Jealousy) while Bosonic states allow infinite stacking.	Multi-agent continuous collision
Topological Inertia	`TopologicalInertia.lean`	Formalizes Newtonian Momentum ( $p=mv$ ); high-momentum routines (Habits) require massive external Charisma ( $F \ge p$ ) to halt or alter.	Speculative execution caching
Topological Desire	`TopologicalDesire.lean`	Formalizes the Wont For Nothing Identity: without external Ghost Mass, the topology is flat and experiences zero gravitational pull (Desire).	Auto-scaling algorithms
Topological Trust	`TopologicalTrust.lean`	Formalizes the Strong Nuclear Force; Trust confines states against external repulsion. Dogma is an unbreakable bind.	Distributed execution consensus
Topological Dark Energy	`TopologicalDarkEnergy.lean`	Formalizes Cosmological Expansion; uncoupled states distance natively over time unless counteracted by active Gravity. Includes DarkEnergySandwich.	Cosmic graph expansion
Topological Induction	`TopologicalInduction.lean`	Formalizes Electromagnetic Induction; state changes induce propagation waves bounded by resistance. Includes InductionSandwich.	Gossip/Broadcast ripples
Topological Turbulence	`TopologicalTurbulence.lean`	Formalizes fluid transition from Laminar to Turbulent routing due to congestion/Reynolds thresholds. Includes TurbulenceSandwich.	Non-linear latency cascades
Discrete mesh compaction (`Fin n`)	`MeshCompaction.lean`	Mask pruning, iterated prune fixed point, `ℕ` logits masks anti-monotone in `τ`, `Finset`-fold decidable quotient pushforward (`Bool.or` over `Fin n × Fin n`), gauge edge activity non-increase under prune	Softmax / DSAE cost atoms (kept separate by design)

Particle / gravity narrative closures (e.g. LocalGravityLaw.lean, ParticleTheoryCoreClosure.lean) live in the main ForkRaceFoldTheorems graph. They are not automatically part of PhysicsSandbox; link them manually when a story needs both Mathlib analysis and Gnosis bookkeeping.

Axiom discipline

Physical postulates should follow the same pattern as cryptographic extrinsic claims: named opaque / axiom blocks with documented interfaces — no anonymous sorry on promoted surfaces.

CI / build

Default: lake build still targets ForkRaceFoldTheorems (full corpus).
Focused physics hub: lake build PhysicsSandbox (also pnpm run validate:physics-sandbox from open-source/gnosis).
GitHub Actions: .github/workflows/gnosis-physics-sandbox.yml runs on pushes/PRs that touch the physics Lean paths above.

forkjoin-ai/gnosis