Formal reconstruction · Inflationary spectra, one-sky sampling variance, fixed-weight beam design, conditional likelihood precision, a limited consistency test, cosmological corrections, and cosmic confusion
Determination of Inflationary Observables by Cosmic Microwave Background Anisotropy Experiments
How an ensemble prediction becomes a noisy inference from one sky, why perfect detectors do not remove cosmic variance, and why small conditional error bars need not survive cosmological nuisance uncertainty
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureProof-free data selected by one sampling-variance calculation. Besides the four physical indices, the model retains exactly the ten maps and proposition-valued relation families used by the shared route.
- inductiveOnly physical claims common to the two sampling-variance routes transfer. Gaussian moments, chi-square laws, survey-area scaling, scan geometry, beam response, likelihoods, and forecast errors are not constructors.
- structureThe mechanism-neutral physical indices selected by the repeated route.
- structure
- structureThe shared constraint paired with one typed paper-local derivation.
- structurePaper-local meanings for the selected calculation, its containing cosmological/statistical theory, and the one physical realization it represents.
- structurePositive sampling variance for the selected one-realization estimator.
- structureThe containing cosmological theory is distinct from the calculation.
- structureThe one represented physical realization remains distinct from both.
- structureThe observation measure may be angular area or counting measure on real harmonic degrees of freedom. Noise power is subtracted before calibration.
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- structureEquations (17)-(18): baryon uncertainty induces different parameter shifts.
- structureEquation (4) evaluated for two beam widths at genuinely fixed weight.
- structurePaper-local physical data and relations. Proposition fields describe physical or inferential relations; they do not contain proofs of the paper's desired conclusions.
- structure
- structureSame two-point power can hide different non-Gaussian fourth moments.
- structure
- structure
- structureEquations (6), (25), (31), and (32): the actual chi-square likelihood.
- structureManuscript p. 7: pixel noise and detector weight have different scaling.
- structurePaper-local value readout for Knox's author-manuscript p. 8 equations (4)-(5). The multipole remains an integer index, while the angular power, weight per solid angle, Gaussian beam width, estimator variance, relative uncertainty, and explicit noise-free limiting variance are real-valued readouts. The full estimator distribution and map construction remain separate imported calculations.
- structureForeground cleaning increases variance and can create pixel correlations.
- structureEquations (2)-(3): full-sky isotropic harmonic covariance and mode count.
- structureThe physical sky and detector-noise realization are distinct. The sky ensemble is the first marginal of this joint experiment ensemble.
- inductiveThe paper-local stochastic route used for the shared variance result.
- structureManuscript p. 21: both correction factors are squared quadrupole ratios.
- structure
- structure
- structureA deliberately weak statement that a quantity is available on a selected system in a selected regime. It does not name an observer, procedure, apparatus, prediction, or physical-existence claim. Papers that supply those stronger roles should use the corresponding contexts below and may project to this weaker relation only when that loss of information is intended.
- structure
Definitions and domain choices
- definitionActual first and raw second moments of a normalized, square-integrable estimator. Source-specific Gaussian and angular calculations supply these equalities; neither positive variance nor distinct estimates is a field.
- definition
- definition
- definitionThe statistical ensemble must describe physically possible realizations on which the selected observable is available.
- definitionThe complete realized sampling-variance result at one proof-free model. This direct proposition is stronger than the implication-valued estimator calculation: it contains a selected realization that is the only observed one and is possible, accessible, and noise-excluded; the realized unbiasedness, law, variance, and positive-variance outputs; two possible realizations with different estimates; the resulting sampling variation; and the failure of exact ensemble recovery. The ensemble target remains part of the final recovery statement, although changing that target cannot erase variation once two possible estimates are already different.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA real-valued reading of the actual selected estimator. The estimate type need not itself be `Real`, and no injectivity of this reading is assumed.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe inhabited pre-calculation content of the exactly selected sampling model. Estimator-law, variance, positivity, realization-variation, and recovery outputs are not included.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique calculation model selected by this paper-local context.
- definition
- definition
- definition
- definition
- definitionSource-sensitive explanation retains a typed paper-local calculation in addition to the common one-realization estimator route.
- definitionOrdinary structural explanation by the complete shared technical route.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExplicit convergence and normalization inputs, not a variance formula.
- definitionGaussianity can supply this identity, but the identity does not specify a full Gaussian law or the distribution of the quadratic statistic.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definitionEvery route named in the supplied identifier list is semantically certified.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe noise-free full-sky estimator's first and raw second moments, attached to an actual normalized sky measure. The `C_l^2 + variance` second moment is the precise mathematical output needed from the Gaussian mode calculation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionCleaning increases scalar noise while leaving nonzero cross-pixel noise.
- definitionFine and coarse pixels have equal observing weight but different noise.
- definition
- definition
- definitionAn independent binary signal and binary detector, used only as a calibration diagnostic, not as a Gaussian full-sky CMB ensemble.
- definition
- definitionA doubled scalar quadrupole has `f_S=4`, while the tensor keeps `f_T=1`.
- definition
- definition
- definitionA negative, interior estimator value at `ell=3` obeys the full printed likelihood with seven real degrees of freedom and its exact Jacobian.
- definition
- definition
- definition
- definitionEquation (4) compares beam widths zero and one at `l=2,w=C_l=1`.
- definition
- definitionThe full-sky quadrupole has exactly five independent harmonic modes.
- definitionAppendix equation (31) gives `V=5` when estimate and ensemble power agree.
- definition
- definitionTen-percent baryon uncertainty exceeds both original conditional errors.
- definition
- definition
- definition
- definition
- definitionOriginal appendix inputs: harmonic field moments, the separate full Gaussian mode law, physical readout identification, and the other source calculations. Estimator variances and variation are derived downstream.
- definitionThe selected formula readout must belong to the same experiment, multipole, Gaussian beam, model power spectrum, and physical variance readouts used by the paper-local estimator route.
- definition
- definitionJoint Gaussian mode law is stronger than a fourth-moment identity and is required separately for the full estimator distribution.
- definitionImported harmonic projection and Gaussian moment calculations, including the real-sky identification of `2*l+1` real, not independent complex, modes. Neither estimator variance nor sampling variation occurs among the inputs.
- definitionThe zero-noise sky is a marginal, not a noisy detector realization. The variance readouts refer to the corresponding actual quadratic statistics.
- definition
- definition
- definition
- definition
- definitionLower-level realization of already identified estimator outputs. This moment bridge alone does not reconstruct the source's harmonic sky map.
- definition
- definition
- definition
- definitionThe likelihood variable uses the selected multipole, beam, and weight.
- definitionThe source formula package ties the printed equations to the selected physical experiment before a named estimator calculation may consume them.
- definitionBoth beam experiments obey the printed detector-weight equations.
- definitionThe appendix's harmonic modes belong to the same selected power spectrum.
- definitionEquation (16) uses the same selected correction factors and observables.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionKnox's multipole-access relation is a sky-scoped availability claim, not an observer/procedure claim. A sky is included only when it is a possible realization of the selected model regime.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAppendix (31)-(32) for any physical multipole. Noise subtraction moves the lower endpoint to minus the beam-deconvolved noise, not to zero. The normalization includes the change-of-variable Jacobian.
- definitionA restricted nonnegative quadrupole diagnostic, not the general estimator law used by the primary route.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAuthor manuscript p. 8, equation (5): the relative uncertainty rewrites the same variance using the printed `l^2 C_l` form. The duplicated `l^2` factors are retained instead of silently simplifying the source expression.
- definitionAuthor manuscript p. 8, equation (4): the diagonal estimator variance is the sampling factor `2/(2l+1)` times the square of angular power plus the beam-deconvolved noise term.
- definitionThe explicit `w = infinity` (`sigma_pix = 0`) limit stated immediately after equation (4). It is a selected noise-free source value, not a claim that a finite real detector weight equals infinity.
- definitionThe source works with physical multipoles `l >= 2`, positive angular power, positive finite detector weight, and a nonnegative Gaussian beam width.
- definitionThe complete selected equation-(4)/(5) source formula package.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAn inhabited full-sky quadrupole with unit power and detector weight.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThis is an affine Gaussian-square law, not a bare chi-square law.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAppendix equations (26)-(30): beam-smoothed signal plus detector noise, followed by subtraction of the noise mean power and beam deconvolution.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAvailability of a selected sector is substantive only when the sector contains an actual available quantity. The universal clause alone is intentionally kept as a weaker, potentially vacuous relation.
- definition
- definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definition
- definition
- definition
- definition
- definition
- definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
- definition
- definition
- definition
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statementRaw paper inputs construct certificates for every Knox 1995 route.
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- recursor
- definition
- checked statement**Alias** of `PhysicsLogic.Papers.Knox1995.SemanticContext.all_routes_are_semantically_realizable`. --- Raw paper inputs construct certificates for every Knox 1995 route.
- checked statement
- definition
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAppendix (28)-(30) and the Wick mode calculation give both equation (4) and its separate noise-free limit. Neither variance is assumed.
- checked statement
- checked statementPositive angular power activates the same correlation-based sampling contract for the physical sky and for the separately calibrated noisy map.
- checked statement
- checked statement
- checked statementPrimary anchors: Knox 1995 pp. 3, 5, 7-8 separates ensemble quadrupoles from one sky, selects the full-sky Gaussian-beam setup, and computes a nonzero noise-free estimator variance. The shared direct result retains the actual full-sky setup, realized estimator outputs, distinct possible sky estimates, and the resulting exclusion of exact ensemble recovery without importing Knox's chi-square law as generic physics.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA named estimator-variance output does not supply the printed equation-(4) and equation-(5) source package or its positive noise-free limit.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
Every premise, numerical forecast, dependency, qualification, and non-implication below comes only from Knox1995.lean, SourceMap.lean, and Coverage.lean. Spectrum evolution, map construction, estimator distributions, likelihood recovery, tensor-tilt sensitivity, cosmological correction factors, foreground treatment, and nuisance shifts remain named proposition-valued inputs; the manuscript's equations (4)-(5) are separately retained as a source-local real-valued formula package and exposed by an explicit route claim derived from the selected sky setup and estimator calculation. The edition does not turn an ensemble mean into the observed sky, a noise-free instrument into an exact cosmological measurement, or a fixed-cosmology forecast into a total uncertainty.
A forecast becomes meaningful only through its full dependency chain
The seven routes preserve manuscript order without manufacturing a dependency chain. Spectrum parameterization, single-sky variance, instrument comparison, likelihood recovery, consistency testing, and numerical cosmological correction are source-local calculations. Only the final nuisance route consumes the checked likelihood precision, so its main conclusion compares nuisance shifts against the conditional statistical forecast rather than replacing it.
| Transition | Status | Retained boundary |
|---|---|---|
| Inflationary setup to power-law observables | deferred spectrum calculation | The parameterization and near-scale-invariance outputs are supplied, not rederived. |
| One full sky to estimator variance | deferred estimator calculation | Noise exclusion and positive sampling variance are separate facts. |
| Fixed-weight beam comparison | calculation + controlled foreground scope | Realistic frequency and spatial foreground correlations are explicitly absent. |
| Likelihood to three forecast errors | fixed-cosmology forecast | The background cosmological parameters are held fixed. |
| Consistency relation to practical test | deferred sensitivity + interpretation | A valid relation does not guarantee that the predicted tensor tilt is distinguishable from zero. |
| Nonzero cosmological constant to corrected relation | numerical correction calculation | The scalar and tensor response factors are explicit computational inputs. |
| Statistical precision to satellite capability | nuisance calculation + author expectation | Nuisance shifts dominate; higher-multipole degeneracy breaking is only expected. |
Inflation supplies four observables, but quadrupoles remain ensemble quantities
The selected model is inflationary and carries scalar and tensor primordial spectra. Background cosmological parameters are fixed for the forecast. A supplied spectrum calculation makes both spectra approximately power law and nearly scale invariant, then identifies scalar amplitude, tensor ratio, scalar tilt, and tensor tilt as observables of the model.
→ approximately power-law, nearly scale-invariant spectra
→ scalar amplitude, tensor ratio, scalar tilt, tensor tilt. deferred spectrum parameterization; author manuscript p. 2, equation (1) (1)
The same output identifies the scalar amplitude and tensor ratio as ensemble quadrupole parameters. It explicitly denies that the scalar amplitude is an actual-sky quadrupole parameter. This is the first guardrail: a parameter of the probability distribution over skies is not the measured value on every possible realization.
scalar amplitude: not an actual-sky quadrupole parameter,
therefore ensemble prediction ≠ realization-by-realization identity. the formal negation is asserted explicitly for the selected scalar-amplitude parameter (2)
The checked theorem returns all four observable classifications and preserves the exact ensemble/actual-sky distinction.
spectrum_calculation_yields_power_law_observables · author manuscript pp. 2–3A perfect measurement of one sky still has cosmic variance
Select Gaussian perturbations, a full-sky experiment, the observed sky as a possible realization of the model, and an accessible multipole. The main calculation now uses actual real harmonic amplitudes, with a physical sky and detector realization kept separate. Lean derives the mean and variance from their correlations and Wick fourth moments. The full affine Gaussian-square estimator law requires a separate Gaussian mode-law input.
Xi = exp(−b/2) Si + Di, Ĉℓ = exp(b) [n−1 ΣiXi2 − N].
Signal temperature-variance contribution = n Cℓ Wℓ/(4π).
The noise-free sky ensemble is the sky marginal of the joint experiment measure.
HarmonicSkyMap · HarmonicObservationAt · equation (3) and appendix equations (26)-(30)
ΔCℓ/Cℓ = √[2/(2ℓ+1)] [1 + ℓ2w−1exp(ℓ2σb2)/(ℓ2Cℓ)],
w = ∞ (σpix = 0) → (ΔCℓ)2 = 2Cℓ2/(2ℓ+1) > 0 → cosmic variance remains. Integer ℓ ≥ 2 and positive Cℓ; harmonic projection and Gaussian moment evaluation remain inputs, while the mode-to-estimator mean and variance are checked deductions. (3)
single_sky_setup_retains_printed_harmonic_covariance_and_mode_count · physical_quadrupole_realizes_printed_variance_and_cosmic_variance
Full-sky coverage is an actual source hypothesis, not an automatic conclusion about a half-sky experiment. Nor does equal angular power determine higher moments without the independently retained Gaussian assumption: two checked mode distributions have the same second moment 1 but distinct fourth moments 1 and 4.
Positive actual noise-free variance, together with ensemble support on possible accessible skies, now derives two different possible-sky estimates. That witness is not supplied independently. It excludes exact recovery of the ensemble target from every realization. A known noise-mean subtraction does not remove sampling fluctuations.
harmonic_field_calculation_derives_estimator_outputs
Ĉ = (S+D)2 − 1 has E[Ĉ] = 1, but Ĉ(−1,+1) = −1. A calibrated finite detector diagnostic, not a Gaussian full-sky ensemble.
actual_noise_mean_subtraction_does_not_preserve_pointwise_nonnegativity
→ no rule recovers the ensemble target from every realization,
even in the detector-noise-free limit. single-realization obstruction, not a claim of estimator bias (4)
The theorem keeps noise exclusion, positive variance, the name “cosmic variance,” failure of universal ensemble recovery, and the selected equation-(4)/(5) formula package in one conclusion.
noise_free_measurement_retains_cosmic_variance · noise_free_cosmic_variance_retains_selected_formula_package · author manuscript pp. 3, 5–8, 25–26The typed route fullSkyChiSquareNoiseFreeVariance preserves that Gaussian full-sky setup and the estimator calculation as source evidence. EstimatorVarianceFormulaReadout ties the printed values to the selected experiment, multipole, Gaussian beam, angular power, detector weight, and represented variance values before that calculation can return them. equation_four_noise_free_limit_is_positive checks the positive limit, while named_estimator_output_does_not_supply_printed_formula_package blocks a name-only estimator predicate from masquerading as equations (4)-(5).
knox_source_inputs_make_shared_sampling_variance_route_applicable constructs the common route, while knox_source_inputs_realize_structural_sampling_variance_explanation and knox_source_inputs_realize_source_structural_sampling_variance_explanation distinguish the ordinary and source-sensitive explanations. Neither theorem treats the already established cosmic-variance conclusion as its derivation, and the shared framework does not inherit Knox's CMB normalization conventions.
At fixed detector weight, finer angular resolution never loses precision
Compare two full-sky experiments with Gaussian beams and the same total detector weight. One beam is narrower. The supplied beam-dependent variance calculation says that the narrow-beam experiment is no worse at every multipole and strictly better at high multipoles. The broader beam can be synthesized from the finer-resolution data.
→ narrow-beam precision no worse at every multipole,
→ strictly better at high multipoles,
→ wide beam synthesizable from narrow-beam data. fixed-weight comparison; author manuscript pp. 7 and 9 (5)
Fine pixels: solid angle 1/4, time 1, noise variance 4, weight 1. Coarse pixels: solid angle 1/2, time 2, noise variance 2, weight 1. Beam variances: 8/5 and (2/5)(1+exp(4))^2.
beam_route_retains_detector_weight_beam_and_foreground_equations
The result is deliberately not advertised as a universal instrument theorem. A foreground model and multifrequency separation are included, and foregrounds degrade the effective noise. Realistic foreground frequency and spatial correlations are explicitly not included in that model.
The physical foreground witness has clean pixel variance 1, degraded variance 4, actual cross-pixel covariance 1/2, and simplified covariance 0. A scalar effective-noise correction therefore does not establish independent foreground-cleaned pixels.
The theorem returns the all-multipole ordering, strict high-multipole gain, beam-synthesis fact, foreground noise degradation, and omitted-correlation qualification.
fixed_weight_smaller_beam_improves_multipole_precision · author manuscript pp. 7–9The reported precision is a fixed-cosmology likelihood forecast
The likelihood route selects a full-sky experiment and likelihood for the chosen model while holding the cosmological parameters fixed. A supplied maximum-likelihood and simulation calculation produces the three reported uncertainties. The source map anchors them to the selected 20-arcminute forecast.
→ uncertainty in scalar tilt = 0.016,
→ uncertainty in tensor ratio = 0.11,
→ relative uncertainty in pivot amplitude = 0.003,
with pivot amplitude uncorrelated with scalar tilt. conditional likelihood and Monte Carlo calculation; manuscript pp. 10–13 and 17 (6)
V = n(Ĉℓ+Nb)/(Cℓ+Nb), Ĉℓ ≥ −Nb.
p(Ĉℓ) = n Vn/2−1 exp(−V/2) / [(Cℓ+Nb) 2n/2 Γ(n/2)] for V > 0; p = 0 at the lower endpoint.
RetainsPrintedEstimatorLikelihood · appendix (31)-(32), including the Jacobian
likelihood_recovery_retains_original_chi_square_density
general_estimator_likelihood_allows_negative_nonquadrupole_estimates
Choosing the pivot amplitude removes the selected amplitude–tilt correlation, but it does not relax the fixed-cosmology premise. The formal result is therefore named scoped parameter precision. It is a statistical forecast inside the selected model, not a claim that all cosmological and foreground uncertainties are smaller.
The theorem returns the fixed-cosmology condition, all three forecast uncertainties, and the pivot decorrelation.
likelihood_calculation_yields_scoped_parameter_precision · author manuscript pp. 10–13, 17A valid consistency relation can still be a weak observational test
The selected consistency test uses tensor ratio r = 1 and tensor tilt nT = −1/7, which satisfy the lowest-order inflationary relation. A supplied sensitivity calculation says the tensor lever arm is limited and the predicted tilt is not distinguished from zero. The paper's interpretive output is that a significant deviation is required for a useful falsification test.
but limited tensor lever arm → predicted nT not distinguished from zero,
→ significant deviation needed to falsify the relation. deferred tensor-tilt calculation plus interpretive testing criterion; manuscript pp. 17–20 (7)
A nonzero cosmological constant then changes the mapping from primordial quantities to low-multipole anisotropies. The late integrated Sachs–Wolfe effect changes the scalar low multipoles, while tensor low multipoles are only weakly affected. A Boltzmann-code calculation supplies separate scalar and tensor correction factors.
r = −7 [fT / fS] nT. numerically computed correction factors; manuscript pp. 20–21, equation (16) (8)
cosmological_correction_retains_both_squared_quadrupole_ratios
One theorem separates truth of the lowest-order relation from its weak distinguishability; the other returns the unequal low-multipole responses, numerical correction factors, and corrected relation with its minus sign.
limited_tensor_lever_arm_weakens_consistency_test · cosmological_constant_requires_corrected_consistency_relation · manuscript pp. 17–21Cosmological nuisance uncertainty can dominate the statistical precision
The final route relaxes the assumption of perfectly known background cosmology. It selects a nuisance cosmological parameter that is uncertain and shifts both the scalar-tilt and tensor-ratio forecasts. A supplied confusion calculation says those shifts dominate the corresponding conditional statistical uncertainties.
→ nuisance uncertainty dominates both statistical forecasts. deferred parameter-shift and degeneracy calculation; manuscript pp. 21–22 (9)
The original equations multiply fractional baryon uncertainty by
1/4 for scalar tilt and 13/10 for tensor ratio. At fractional
uncertainty 1/10, the induced shifts 1/40 and 13/100 exceed the
conditional errors 16/1000 and 11/100, respectively.
cosmic_confusion_retains_printed_baryon_response_coefficients · author manuscript p. 22, equations (17)–(18)
The independent certificate has 20 physically inhabited boundaries, covering full-sky mode counts, non-Gaussian higher moments, pixel versus detector noise, beam calculations, chi-square likelihoods, correlated foregrounds, squared cosmological corrections, and baryon nuisance response.
The calculation also returns that higher multipoles may lift the degeneracy. The source map classifies that last statement as an author expectation. It is part of the conditional capability result, but it is not a demonstrated degeneracy-removal theorem.
The main theorem combines the scoped precision with nuisance dominance for scalar tilt and tensor ratio and the higher-multipole outlook. It does not convert that outlook into established parameter separation.
nuisance_uncertainty_can_dominate_statistical_precision · author manuscript pp. 21–24Concept guide
Inflationary observables
The selected scalar amplitude, tensor ratio, scalar tilt, and tensor tilt obtained from approximately power-law scalar and tensor spectra.
PowerLawObservableDescriptionEnsemble quadrupole parameter
A parameter of the distribution over possible skies, explicitly separated from an actual-sky quadrupole parameter.
ensembleQuadrupoleParameterCosmic variance
The positive sampling variance remaining for a full-sky estimator when instrumental noise at the selected multipole is absent, with the selected equation-(4)/(5) value package retained.
NoiseFreeCosmicVarianceConclusionSingle-sky estimator
The unbiased chi-square-distributed estimate calculated from one possible observed sky rather than from an ensemble of skies; its paper-local readout retains the printed variance and relative-uncertainty formulas.
EstimatorVarianceCalculation · EstimatorVarianceFormulaReadoutFixed-weight beam comparison
The comparison of two full-sky Gaussian-beam experiments with equal total detector weight and different angular resolution.
AngularResolutionSetupForeground qualification
Multifrequency separation degrades effective noise while realistic frequency and spatial correlations remain outside the calculation.
AngularResolutionCalculationScoped parameter precision
The three reported likelihood uncertainties under the explicit condition that background cosmology is fixed.
ScopedParameterPrecisionPivot amplitude
The selected amplitude parameter whose forecast is uncorrelated with scalar tilt in the likelihood calculation.
pivotAmplitudeUncorrelatedWithTiltLowest-order consistency relation
The relation r = −7nT, retained separately from the experiment's ability to distinguish the predicted tensor tilt from zero.
lowestOrderConsistencyRelationLimited tensor lever arm
The restricted angular-scale leverage that weakens the selected tensor-tilt consistency test.
ConsistencyTestCalculationCosmological-constant correction
The unequal scalar and tensor low-multipole response factors that modify the quadrupole consistency relation.
correctedConsistencyRelationCosmic confusion
Nuisance cosmological uncertainty whose induced parameter shifts dominate the conditional scalar-tilt and tensor-ratio forecasts.
CosmicConfusionCalculationConditional satellite capability
The main conclusion combining fixed-cosmology precision, nuisance dominance, and the expected possibility of higher-multipole degeneracy breaking.
ConditionalSatelliteCapabilityShared sampling-variance model
The reusable single-realization framework grounded in the selected cosmological model, observed sky, multipole, and full-sky experiment.
selectedSamplingVarianceContextComplete route inventory, non-implications, and provenance
The source map declares seven routes, thirty-eight claims, and thirty-eight sourced steps. Coverage assigns paper-local semantics to every atom and certifies each route. The main conclusion is the conditional satellite capability; the other route outputs remain separately available rather than being hidden inside one undifferentiated forecast.
| Route | Direct dependencies | Declared outputs | Profile |
|---|---|---|---|
| Spectra and observables | — | Power-law parameters; ensemble distinction | deferred spectrum calculation |
| Cosmic variance | — | Estimator law; residual variance; equation-(4)/(5) formula package; cosmic variance; no exact recovery | deferred estimator calculation |
| Experiment design | — | All-multipole ordering; high-ℓ gain; beam synthesis; foreground scope | fixed-weight comparison |
| Likelihood recovery | — | Scoped precision; pivot decorrelation | fixed-cosmology forecast |
| Consistency test | — | Relation; limited lever arm; zero-tilt non-distinction; falsification requirement | controlled + interpretive |
| Cosmological correction | — | Response difference; numerical factors; corrected relation | numerical calculation |
| Confusion and scope | Likelihood recovery | Nuisance dominance; conditional capability; expected high-ℓ relief | deferred + expected |
Spectra and observables · spectra_and_observables_route_is_semantically_realized
Cosmic variance · cosmic_variance_route_is_semantically_realized
Experiment design · experiment_design_route_is_semantically_realized
Likelihood recovery · likelihood_recovery_route_is_semantically_realized
Consistency test · consistency_test_route_is_semantically_realized
Cosmological correction · cosmological_correction_route_is_semantically_realized
Confusion and scope · confusion_and_scope_route_is_semantically_realized
Four formally blocked shortcuts
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| A named estimator-variance output | Knox's printed equation-(4)/(5) values or positive noise-free limit | named_estimator_output_does_not_supply_printed_formula_package |
| Every selected sky is detector-noise-free | All possible skies give the same estimate or identify the ensemble target | noise_free_skies_need_not_identify_ensemble_target |
| A positive conditional statistical precision | Nuisance-induced shifts are smaller than the forecast uncertainty | statistical_precision_does_not_exclude_nuisance_dominance |
| The test point satisfies r = −7nT | The predicted tensor tilt is experimentally distinguishable from zero | a_consistency_relation_does_not_make_it_distinguishable |
The four witnesses retain source-shaped numerical distinctions. The named estimator readout has physical multipole, angular-power, detector-weight, and beam-width domain data while its equation-(4)/(5) outputs are wrong. Two positive normalized sky weights give distinct detector-noise-free estimates and their unbiased ensemble target. A positive conditional forecast uncertainty is smaller than a nuisance-induced shift, and the valid tensor relation remains below the selected experimental resolution. No constant proposition, sky-label truth table, or assumed countermodel conclusion is used.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify graph structure. every_source_claim_has_semantics covers all thirty-eight claims, and route_semantic_realization_is_exhaustive covers all seven routes. cosmic_variance_route_exposes_estimator_formula_package checks the explicit estimatorFormula output and its selected-input retention step, while cosmic_variance_result_retains_selected_estimator_formula_package supplies the equation-(4)/(5) package in coverage. noise_free_variance_depends_on_estimator_calculation, forecast_precision_retains_fixed_cosmology_scope, corrected_relation_retains_numerical_calculation, and final_capability_retains_confusion_and_expectation preserve the remaining calculation and scope boundaries.
Lean-encoded bibliographic record
L. Knox, Determination of Inflationary Observables by Cosmic Microwave Background Anisotropy Experiments (1995), original astro-ph/9504054v1 manuscript.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems (76)
gaussian_mode_law_determines_affine_estimator_distributionequation_four_noise_free_limit_is_positivephysical_quadrupole_realizes_printed_variance_and_cosmic_variancenamed_estimator_output_does_not_supply_printed_formula_packageprinted_full_sky_sampling_retains_real_mode_countprinted_full_sky_sampling_retains_five_quadrupole_modesprinted_quadrupole_likelihood_has_five_degrees_of_freedomselected_estimator_formula_package_exposes_positive_noise_free_variancesampling_variance_model_retains_exact_paper_semanticsactual_noise_free_harmonic_moments_determine_varianceactual_noise_free_harmonic_moments_are_unbiasedactual_noise_free_variance_realizes_sampling_variationactual_noise_free_variance_excludes_exact_ensemble_recoveryspectrum_calculation_yields_power_law_observablessingle_sky_setup_retains_printed_harmonic_covariance_and_mode_countobserved_sky_realizes_nonvacuous_available_multipole_sectorharmonic_moments_exhibit_nonvacuous_sky_and_map_samplingharmonic_moments_derive_unbiased_sky_and_map_estimatorsharmonic_moments_derive_equation_four_and_noise_free_limitgaussian_map_modes_derive_the_affine_estimator_lawharmonic_field_calculation_derives_estimator_outputssingle_sky_setup_realizes_shared_sampling_variance_setupknox_estimator_outputs_make_shared_route_applicableknox_estimator_variance_makes_shared_route_applicableknox_source_inputs_make_shared_sampling_variance_route_applicableknox_source_inputs_realize_structural_sampling_variance_explanationknox_source_inputs_realize_source_structural_sampling_variance_explanationknox_estimator_variance_realizes_shared_routeknox_estimator_variance_exhibits_nonvacuous_shared_sampling_variancemeasure_grounded_estimator_moments_reconstruct_estimator_outputsmeasure_grounded_estimator_route_exhibits_nonvacuous_sampling_varianceknox_estimator_variance_realizes_every_shared_sampling_variance_claimknox_sampling_variance_model_establishes_theory_model_groundingknox_estimator_variance_establishes_theory_model_grounded_sampling_varianceknox_estimator_variance_transfers_every_shared_sampling_variance_claimnoise_free_measurement_retains_cosmic_variancenoise_free_cosmic_variance_retains_selected_formula_packageestimator_route_retains_printed_chi_square_likelihood_variablefixed_weight_smaller_beam_improves_multipole_precisionbeam_route_retains_detector_weight_beam_and_foreground_equationslikelihood_calculation_yields_scoped_parameter_precisionlikelihood_recovery_retains_original_chi_square_densitylimited_tensor_lever_arm_weakens_consistency_testcosmological_constant_requires_corrected_consistency_relationcosmological_correction_retains_both_squared_quadrupole_ratiosnuisance_uncertainty_can_dominate_statistical_precisioncosmic_confusion_retains_printed_baryon_response_coefficientsfinite_signal_plus_noise_estimator_retains_actual_calibrationactual_noise_mean_subtraction_does_not_preserve_pointwise_nonnegativitygeneral_estimator_likelihood_allows_negative_nonquadrupole_estimatesfull_sky_quadrupole_realizes_original_five_mode_covarianceprinted_full_sky_harmonic_sampling_is_not_restricted_to_the_quadrupolefive_exactly_measured_full_sky_modes_do_not_remove_cosmic_variancefinite_detector_weight_does_not_realize_the_zero_noise_limitpartial_sky_power_does_not_supply_full_sky_cosmic_variance_domainfull_sky_coverage_does_not_supply_the_printed_mode_countoriginal_detector_weight_stays_fixed_while_pixel_noise_changesfixed_detector_weight_does_not_mean_equal_pixel_noiseoriginal_fixed_weight_beams_realize_both_variance_equationsoriginal_narrower_beam_strictly_reduces_quadrupole_varianceequal_detector_weight_does_not_make_distinct_beams_equally_precisea_narrower_beam_without_variance_calculation_does_not_improve_precisionoriginal_quadrupole_likelihood_realizes_five_degree_chi_squarea_named_positive_likelihood_does_not_supply_its_chi_square_mode_counta_correct_mode_count_does_not_supply_the_printed_likelihood_variableforeground_cleaning_realizes_degradation_and_omitted_pixel_correlationscalar_foreground_degradation_does_not_remove_pixel_correlationsa_zero_simplified_foreground_covariance_does_not_describe_actual_noisecosmological_constant_realizes_distinct_squared_quadrupole_correctionscorrected_inflationary_relation_does_not_imply_uncorrected_relationnamed_scalar_tensor_factors_do_not_supply_squared_quadrupole_ratiosoriginal_baryon_response_exceeds_both_conditional_forecast_errorsidentical_angular_power_without_gaussianity_does_not_fix_higher_momentsnoise_free_skies_need_not_identify_ensemble_targetstatistical_precision_does_not_exclude_nuisance_dominancea_consistency_relation_does_not_make_it_distinguishable
Coverage theorems (10)
every_source_claim_has_semanticsspectra_and_observables_route_is_semantically_realizedcosmic_variance_result_retains_selected_estimator_formula_packagecosmic_variance_route_is_semantically_realizedexperiment_design_route_is_semantically_realizedlikelihood_recovery_route_is_semantically_realizedconsistency_test_route_is_semantically_realizedcosmological_correction_route_is_semantically_realizedconfusion_and_scope_route_is_semantically_realizedall_routes_are_semantically_realizable
Source-map audit theorems (18)
argument_wellFormedargument_auditableroutes_wellFormedcosmic_variance_route_exposes_estimator_formula_packageroutes_have_exact_predecessor_graphroutes_have_exact_dependency_closureroutes_expose_only_terminal_outputsearly_source_inputs_and_contracts_are_premise_freelate_source_inputs_and_contracts_are_premise_freeearly_result_steps_apply_exact_semantic_inputsforecast_result_steps_apply_exact_semantic_inputsconsistency_and_correction_result_steps_apply_exact_semantic_inputsconfusion_result_steps_apply_exact_semantic_inputsdependent_routes_consume_certified_predecessor_outputsnoise_free_variance_depends_on_estimator_calculationforecast_precision_retains_fixed_cosmology_scopecorrected_relation_retains_numerical_calculationfinal_capability_retains_confusion_and_expectation
Semantic atoms (38)
inflationaryObservableSetupinflationarySpectrumCalculationpowerLawObservableDescriptionensembleQuadrupoleDistinctionsingleSkyEstimatorSetupestimatorVarianceCalculationunbiasedChiSquareEstimatorpositiveNoiseFreeSamplingVarianceestimatorVarianceFormulaPackagecosmicVarianceConclusionnoExactEnsembleRecoveryangularResolutionSetupangularResolutionCalculationnoWorseAtEveryMultipolestrictlyBetterAtHighMultipoleslargerBeamSynthesisforegroundQualificationlikelihoodForecastSetuplikelihoodRecoveryCalculationscopedParameterPrecisionpivotAmplitudeDecorrelationconsistencyTestSetupconsistencyTestCalculationlowestOrderConsistencyRelationlimitedTensorLeverArmzeroTiltNotDistinguishedsignificantDeviationNeededcosmologicalCorrectionSetupcosmologicalCorrectionCalculationscalarTensorResponseDifferencenumericalCorrectionFactorscorrectedConsistencyRelationcosmicConfusionSetupcosmicConfusionCalculationnuisanceDominatesTiltPrecisionnuisanceDominatesRatioPrecisionconditionalSatelliteCapabilityhigherMultipolesMayLiftDegeneracy
Claim identifiers (38)
observableSetupspectrumCalculationpowerLawDescriptionensembleDistinctionskySetupvarianceCalculationestimatorDistributionresidualVarianceestimatorFormulacosmicVariancenoExactRecoveryresolutionSetupresolutionCalculationallMultipolePrecisionhighMultipolePrecisionbeamSynthesisforegroundScopelikelihoodSetuplikelihoodCalculationstatisticalPrecisionpivotDecorrelationconsistencySetupconsistencyCalculationlowestOrderRelationlimitedLeverArmnoZeroTiltDistinctionfalsificationRequirementcorrectionSetupcorrectionCalculationresponseDifferencecorrectionFactorscorrectedRelationconfusionSetupconfusionCalculationtiltConfusionratioConfusionconditionalCapabilitydegeneracyOutlook
Step identifiers (38)
stateObservableSetupstateSpectrumCalculationderivePowerLawDescriptionderiveEnsembleDistinctionstateSkySetupstateVarianceCalculationderiveEstimatorDistributionderiveResidualVarianceretainEstimatorFormulaPackageidentifyCosmicVarianceexcludeExactRecoverystateResolutionSetupstateResolutionCalculationderiveAllMultipolePrecisionderiveHighMultipolePrecisionderiveBeamSynthesisretainForegroundScopestateLikelihoodSetupstateLikelihoodCalculationderiveStatisticalPrecisionderivePivotDecorrelationstateConsistencySetupstateConsistencyCalculationretainLowestOrderRelationderiveLimitedLeverArmderiveNoZeroTiltDistinctionderiveFalsificationRequirementstateCorrectionSetupstateCorrectionCalculationderiveResponseDifferencederiveCorrectionFactorsderiveCorrectedRelationstateConfusionSetupstateConfusionCalculationderiveTiltConfusionderiveRatioConfusionderiveConditionalCapabilityretainDegeneracyOutlook
Route identifiers (7)
spectraAndObservablescosmicVarianceexperimentDesignlikelihoodRecoveryconsistencyTestcosmologicalCorrectionconfusionAndScope
Route kinds (7)
inflationaryParameterizationsingleRealizationEstimatorfixedWeightInstrumentComparisonconditionalLikelihoodForecastlimitedConsistencyTestnumericalCosmologicalCorrectionnuisanceParameterQualification
Checked source-route details
This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.
spectraAndObservables
Logical kind: inflationaryParameterization.
Required predecessor routes: none.
Ordered inference steps: stateObservableSetup, stateSpectrumCalculation, derivePowerLawDescription, deriveEnsembleDistinction.
Exported conclusions: powerLawDescription, ensembleDistinction.
cosmicVariance
Logical kind: singleRealizationEstimator.
Required predecessor routes: none.
Ordered inference steps: stateSkySetup, stateVarianceCalculation, deriveEstimatorDistribution, deriveResidualVariance, retainEstimatorFormulaPackage, identifyCosmicVariance, excludeExactRecovery.
Exported conclusions: estimatorDistribution, residualVariance, estimatorFormula, cosmicVariance, noExactRecovery.
experimentDesign
Logical kind: fixedWeightInstrumentComparison.
Required predecessor routes: none.
Ordered inference steps: stateResolutionSetup, stateResolutionCalculation, deriveAllMultipolePrecision, deriveHighMultipolePrecision, deriveBeamSynthesis, retainForegroundScope.
Exported conclusions: allMultipolePrecision, highMultipolePrecision, beamSynthesis, foregroundScope.
likelihoodRecovery
Logical kind: conditionalLikelihoodForecast.
Required predecessor routes: none.
Ordered inference steps: stateLikelihoodSetup, stateLikelihoodCalculation, deriveStatisticalPrecision, derivePivotDecorrelation.
Exported conclusions: statisticalPrecision, pivotDecorrelation.
consistencyTest
Logical kind: limitedConsistencyTest.
Required predecessor routes: none.
Ordered inference steps: stateConsistencySetup, stateConsistencyCalculation, retainLowestOrderRelation, deriveLimitedLeverArm, deriveNoZeroTiltDistinction, deriveFalsificationRequirement.
Exported conclusions: lowestOrderRelation, limitedLeverArm, noZeroTiltDistinction, falsificationRequirement.
cosmologicalCorrection
Logical kind: numericalCosmologicalCorrection.
Required predecessor routes: none.
Ordered inference steps: stateCorrectionSetup, stateCorrectionCalculation, deriveResponseDifference, deriveCorrectionFactors, deriveCorrectedRelation.
Exported conclusions: responseDifference, correctionFactors, correctedRelation.
confusionAndScope
Logical kind: nuisanceParameterQualification.
Required predecessor routes: likelihoodRecovery.
Ordered inference steps: stateConfusionSetup, stateConfusionCalculation, deriveTiltConfusion, deriveRatioConfusion, deriveConditionalCapability, retainDegeneracyOutlook.
Exported conclusions: tiltConfusion, ratioConfusion, conditionalCapability, degeneracyOutlook.