No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
207theorem no_cloning_informal :
208 -- Cloning a ledger entry without balancing would violate double-entry
209 -- Therefore quantum states cannot be cloned
210 True := trivial
proof body
Term-mode proof.
211
212/-! ## Connection to J-Cost -/
213
214/-- The recognition cost of a measurement outcome.
215 Higher amplitude → lower cost → higher probability. -/
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
probability
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
amplitude
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
probability
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
amplitude
in IndisputableMonolith.Quantum.DoubleSlit
decl_use
-
probability
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use