Formal reconstruction · bulk/wall regime split · thin-layer reduction · qualified separation · visual evidence · suction intervention
On the Motion of Fluids with Very Small Friction
How a locally negligible viscosity remains decisive at a solid boundary
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structure
- structureThe common small-friction boundary contrast in Prandtl and Blasius. The outer viscous scale is proportional to the friction coefficient, whereas a nonzero wall-velocity jump across a thickness with `delta^2 = friction` leaves an order-one wall contribution.
- structureValue-level velocity data for the common physical boundary problem. The wall may move, as explicitly allowed by Prandtl, while Blasius's stationary wall is a separately checked specialization.
- structureThe coupled reduced equations acting on the selected layer flow.
- structureThe selected reduced equations and their coupled action on the layer flow, separated from the source derivation that explains them.
- structureThe selected full-flow side of one boundary-layer reduction.
- structure
- structureThe selected reduced layer, equations, and boundary data.
- structureProof-free ordinary structure for one boundary-layer reduction. It retains the selected full and reduced descriptions, but no equation-reduction, coupling, or paper-local derivation output.
- structureSource-sensitive refinement of the ordinary boundary-layer constraint. It retains one typed paper-local derivation and its realization relation without making provenance part of ordinary physical explanation.
- inductive
- structurePaper-local relation families and one explicitly selected reduction.
- structure
- structureProof-free selected objects and context-owned relation families.
- structureA paper-local theory containing the exact selected model.
- structureA represented physical situation remains distinct from model and theory.
- 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
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- inductivePrandtl's original thin-wall-layer scaling and omission derivation.
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structureAccessible obtained evidence supporting a model in a declared regime.
- structureModel support plus an independently meaningful explicit-exclusion relation.
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definitionBlasius p. 5 retains this additional normal force in its curved-coordinate order count. This is an explicit leading-coordinate balance input, not a general curvilinear NS theorem.
- definitionExact local Cartesian balances, with genuine derivatives and physical coefficients.
- 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 transition layer recovers the selected outer-flow velocity.
- definitionBlasius's selected solid boundary is stationary in both directions.
- definitionBoth physical wall components and the independent outer-flow matching.
- definitionThe fluid's normal velocity follows the actual wall's normal velocity.
- definitionNo tangential slip relative to the selected, possibly moving wall.
- 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
- definitionSource-sensitive explanation of the coupled layer equations.
- definitionOrdinary route explanation of the coupled layer equations.
- definition
- definition
- definitionThe complete selected input boundary for grounding the boundary-layer model. It fixes the exact context-owned model and requires the governing equation, wall adherence, thin-layer scaling, and pressure inheritance. The reduced momentum equation, reduced continuity equation, and their coupling remain outside this setup.
- definitionDirect occurrence of both reduced equations and their coupled behavior.
- definitionEquality to this model retains every selected index and relation family.
- 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 complete physical reduction route is the ordinary explanatory constraint. The reduced-equation and coupling outputs are not; paper provenance is retained only by the source-sensitive refinement below.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOne actual full/reduced pair, the universal bridge, both reduction outputs, and the exhibited coupled layer equations.
- definitionOne source-sensitive thin-boundary-layer derivational reduction.
- definition
- definitionThe full selected route stated directly on every route-used relation.
- definition
- definitionExact mathematical reduction remains a theorem parameter.
- definition
- definitionAn actual reduced equation pair together with both physical velocity boundaries. This refinement does not assume the selected wall is stationary.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected coupled reduced-equation behavior.
- definitionThe exact output-side coupled reduction selected by one model.
- definitionThe exact selected full-flow description.
- definitionThe exact selected reduced boundary-layer description.
- definitionThe exact ordinary explanatory constraint selected by one model.
- definitionThe exact source-sensitive constraint selected by one reduction model.
- definition
- definition
- definition
- definitionScoped derivational semantics for the thin-layer reduction. Realization keeps the physical low-friction boundary-layer setup. Micro support requires both explicit equation-reduction outputs. Macro exhibition requires the reduced momentum and continuity equations to be coupled on the selected layer flow.
- 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
- 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
- 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
- definitionThe numerical profile calculation must concern these same velocity fields and reduced equations, not an unrelated profile token.
- definitionNo drag or traction value is an input. The source calculation supplies the actual profile, wall regularity, and a positive wall slope.
- definitionProceedings p. 488 requires pressure increase in the direction of the actual outer flow, not merely a positive gradient in an arbitrarily oriented chart. The positive transit-time probe retains both the local directional derivative and an actual pressure increase between the selected physical positions.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-native part of Prandtl's wall-layer argument that is shared with Blasius: governing viscous dynamics, adherence, thin-layer scaling, and pressure inheritance. Equation reduction and coupling are not included.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe source-level p. 487 equation pair, tied to the selected layer flow and outer pressure profile. Positivity of density and the selected viscosity constant keeps the physical coefficients explicit rather than hiding them in the names of abstract equation objects.
- definitionRegularity required for the displayed p. 487 derivatives to denote actual derivatives rather than Lean's totalized `deriv` fallback.
- definitionPrandtl's displayed steady planar tangential-momentum equation on original proceedings p. 487: `rho (u partial_x u + v partial_y u) + partial_x p = k partial_y^2 u`.
- definitionOriginal pp. 486-487: fluid velocity agrees with the solid surface and recovers the selected free-fluid tangential velocity outside the layer.
- definitionPrandtl's displayed steady planar incompressibility equation on original proceedings p. 487: `partial_x u + partial_y v = 0`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected adverse pressure condition fixes its physical profile and scope.
- definitionNecessity is the actual implication from separation to directed pressure rise.
- 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
- definitionOriginal p. 487 uses u=f(y/sqrt(x)); it does not fix a complete decimal value for the drag coefficient. The physical domain has x>0.
- 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 normal derivative `partial v / partial y` of Prandtl's selected steady normal velocity field.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe streamwise pressure derivative `dp / dx` imposed by the free fluid.
- definition
- definition
- definition
- definition
- definitionThe original source derivation retains Prandtl's regime split, short-wall-path scope, and systematic omission calculation, but no completed reduction.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected wall may move; its two velocity components remain separate from the free-fluid tangential velocity reached outside the thin layer.
- 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 normal derivative `partial u / partial y` of Prandtl's selected steady tangential velocity field.
- definitionThe second normal derivative `partial^2 u / partial y^2` retained on the right-hand side of Prandtl's reduced momentum equation.
- definitionThe streamwise derivative `partial u / partial x` of Prandtl's selected steady tangential velocity field.
- 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
- 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
- definitionThis is a physical limit diagnostic, not the source's separated-wake claim.
- 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
- definitionA bridge principle derives a macro behavior from any realizing microdescription that supports it.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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
- 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
- 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
- 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
- inductive
- definition
- instance
- 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
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- 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
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- 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
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- structure
- definition
- instance
- checked statementRaw paper-local inputs construct every Prandtl route in source order.
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- recursor
- definition
- checked statementNo completed route certificate is needed to cover a route identifier.
- checked statement
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- definition
- 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
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- 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 statementAn actual suction-field diagnostic, not a construction of the source's impermeable-wall separated wake or a proof of its flow-pattern transfer.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe separation calculation exposes actual pressure rise before the result.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPrandtl's reduced equations are accompanied by actual matching to both velocity components of the selected wall and to the free-fluid velocity.
- checked statement
- checked statement
- checked statement
- checked statementThe original Prandtl source route realizes the stronger shared endpoint without imposing the stationary-wall specialization used by Blasius.
- checked statement
- checked statementThe necessary-condition law applies to an actual selected separating flow.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe pressure gradient follows the selected flow in either chart orientation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPrandtl's full viscous setup, explicit equation reductions, and coupled layer equations realize the shared scoped derivational-reduction semantics. His separation and short-surface-path conclusions remain paper-local.
- checked statementPrandtl's regime split, short-wall-path scope, and systematic omission calculation make the shared technical route applicable before the completed boundary-layer reduction is packaged.
- checked statementOriginal proceedings pp. 486-487: Prandtl's thin wall-layer scaling and systematic omissions directly realize the shared derivational reduction. The proof does not consume `EstablishedBoundaryLayerReduction` or the shared output-led endpoint.
- checked statementOriginal proceedings pp. 486-487: Prandtl's raw regime, path-scope, and systematic-omission inputs realize the source-sensitive boundary-layer derivational reduction without identifying this original thin-wall-layer argument with Blasius's later imported-program order counting.
- checked statementPrandtl's typed thin-wall-layer derivation refines the ordinary explanation without identifying it with Blasius's imported-program order counting.
- checked statementPrandtl's raw pp. 486-487 route realizes the ordinary structural explanation of the coupled reduced equations without consuming a completed endpoint.
- 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
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
- 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
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- 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
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
- 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
This edition follows the paper-local semantics, its SingularLayerLimit.lean helper and fidelity certificate, the source map, and the exhaustive coverage proof. Route certificates establish predecessor availability only; every nonempty result step recovers its selected physical atoms from ClaimsHold before applying its paper-local bridge.
Small viscosity licenses a regional split, not global deletion
The selected viscous equation and incompressibility describe a flow with relevant inertia and positive but small viscosity. The inviscid description is valid in the bulk only where velocity gradients and accumulated action do not restore viscous importance. Near the wall, the same description is invalid.
free_fluid_inviscid_description_is_regime_restricted makes the two-regime validity contrast explicit. Irrotational admissibility is kept distinct from dynamical preservation: boundary-generated vorticity and cyclic accumulation can still enter the selected flow.
The wall layer has its own reduced mechanics
The source-local reduction retains the full viscous governing equation, wall adherence, tangential wall matching, a thin transition layer, thickness and normal-velocity scaling, negligible transverse pressure variation, outer-pressure inheritance, and the not-too-long surface path. The reduced momentum and continuity equations are separate outputs and must be coupled on the layer flow.
partialx u + partialy v = 0
SteadyPlanarBoundaryLayerEquationFormulaAt; original proceedings p. 487(2a)SteadyPlanarBoundaryLayerEquationFormulaAt ties real-valued tangential and normal velocity fields and the imposed outer pressure to the selected layer flow, requires derivative regularity and positive density and viscosity coefficients, and states the displayed pair itself. established_boundary_layer_reduction_retains_steady_planar_equations checks that the completed local reduction retains it, and the source map now exports it separately as boundaryEquationFormula through boundary_layer_route_exposes_steady_planar_equation_formula. The adapter isolates the eight common input relations in SelectedPrandtlBoundaryLayerReductionSetup. prandtl_source_inputs_make_shared_boundary_layer_route_applicable applies the source calculation with its not-too-long path, negligible-curvature premise, and richer displayed formula still present, then projects only the repeated setup and abstract reduction outputs into the shared route. prandtlBoundaryLayerDerivationObtains separately retains the regime split, short-wall-path scope, and systematic omission calculation as the typed source derivation. prandtl_source_inputs_realize_boundary_layer_derivational_reduction realizes the ordinary derivational reduction, while prandtl_source_inputs_realize_source_boundary_layer_derivational_reduction retains Prandtl's typed thin-wall-layer provenance. prandtl_source_inputs_realize_structural_boundary_layer_reduction realizes ordinary structural explanation without provenance; prandtl_source_inputs_realize_source_structural_boundary_layer_reduction adds the typed derivation as a source-sensitive refinement. None consumes an established endpoint. The separate established_reduction_realizes_shared_boundary_layer_model still constructs the output-led eleven-relation endpoint, from which prandtl_boundary_layer_reduction_realizes_derivational_reduction supplies the older projection. Grounding consumes the setup rather than the reduction outputs.
Actual operators and a controlled discarded-term budget
The selected steady equations now hold on an explicitly nonempty patch in the physical half-plane. They are not silently imposed on all space. The selected velocity fields embed into the shared time-dependent operators with zero time derivatives; the candidate full pressure and imposed outer pressure remain distinct. In the notation below, every partial derivative is computed from an actual field.
R_full = rho A_u + p_x - k (u_xx + u_yy).
R_ret = rho A_u + P_x - k u_yy.
R_ret = R_full + k u_xx + (P_x - p_x).
R_full = 0, |u_xx| <= M, |p_x - P_x| <= delta
imply |R_ret| <= |k| M + delta.Actual derivatives and explicit discarded-term controls; the steady embedding has u_t = 0. This is a residual bound, not an exact reduced equation.(2b)
primitive_steady_balances_realize_nonvacuous_source_residual_control consumes both full planar momentum equations, continuity, the derivative and pressure bounds, and nonzero retained normal diffusion. It derives the controlled residual. The source's exact retained PDE still comes from its separate reduction calculation; no equality of the full and retained physical flows is inferred.
|partial_y p_x| <= B throughout the transverse strip;
|p_x(epsilon) - P_x| <= delta_edge.
R_full = 0 and |u_xx| <= M imply
|R_ret| <= epsilon^2 mu M + epsilon B + delta_edge.
For epsilon > 0, p = epsilon y sin(x/epsilon^2), P = epsilon^2 sin(x/epsilon^2):
|p - P| <= epsilon^2, but |p_x - P_x| = 1 at x = y = 0.The bound requires actual differentiability along the whole strip and separate edge-gradient calibration. The pressure-only counterexample is not asserted to solve the full equations.(2c)
planar_source_normal_balance_bounds_pressure_values_at_second_order separately bounds pressure values across the strip from the planar normal balance and its first-order mechanical remainder. That conclusion alone supplies no mixed-derivative bound. These sufficient quantitative controls expose the logic of omission; neither the original order counting nor this formalization establishes a uniform Navier-Stokes solution limit.
u = x^2 - y^2; v = -2 x y;
p = -(x^2 + y^2)^2/2; P = -(x^2 + epsilon^2)^2/2.
Both full planar momentum equations and continuity hold.
At x = 0, y = epsilon: R_ret = 2 epsilon^2 != 0.An actual full-flow solution with a controlled nonzero residual. This local diagnostic does not supply complete wall and far-field matching.(2d)
The independent fidelity matrix has 16 inhabited boundaries. Its discarded-term controls distinguish a small viscosity coefficient from a small discarded product, small pressure values from small gradient mismatch, and a controlled residual from an exact retained equation. In particular, u = x^2/epsilon^2 has k u_xx = 2 when k = epsilon^2; that profile alone is not asserted to solve the coupled equations.
The flat-plate force is an observable of the same profile
FlatPlateFieldRealizationAt binds the actual similarity velocity to the selected flow, its reduced momentum and continuity equations, and its far-field velocity. FlatPlateWallInputs adds positive geometry, wall regularity, adherence, and a positive one-sided slope. It supplies no force value. actual_flat_plate_profiles_establish_nonvacuous_wall_drag derives the shared physical force result, which the main flat-plate conclusion retains.
u(x,y)=f(y/sqrt(x)); f(0)=0; v(x,0)=0.
C=k*f'_+(0) > 0; tau(x)=k*D_y^+u(x,0)=C/sqrt(x).
D_one=b*integral_0^L tau(x) dx=2*b*C*sqrt(L).
D_identical_two=2*D_one.k is dynamic viscosity; derivatives and the force integral are actual Lean operations. Field realization and profile regularity remain explicit calculation inputs. Doubling requires identically loaded faces, not an arbitrary second wall. The printed 1,1... has no assigned exact value or invented error interval.(2e)
the_prandtl_flat_plate_force_is_the_integral_of_its_profile_shear derives the symmetric two-face functional. This does not equate the incomplete numerical report to that exact value or prove the source's numerical profile calculation.
f_e(y)=1-exp(-y)+e*sin(y/e^2)*exp(-y); f_0(y)=1-exp(-y).
u_e(x,y)=f_e(y); v_e(x,y)=0.
For y >= 0: |u_e-u_0| <= e, and both outer limits are 1.
tau_e=3*(1+1/e); |D_one(e)-D_one(0)|=30/e.
e=1/100 gives velocity error at most 1/100 and force error 3000.Both actual wall forces are positive and finite. These are smooth incompressible snapshots, not asserted steady Prandtl solutions. Uniform velocity accuracy does not supply wall-derivative or force accuracy.(2f)
uniform_velocity_accuracy_does_not_control_the_actual_wall_force is the new fidelity boundary. It keeps actual wall matching, continuity, outer recovery, and force integrals in the retained proposition.
Separation changes the outer flow but retains an open threshold
Once the coupled layer exists, a paper-local calculation may establish separation at an externally fixed location, emission of wall-generated vorticity, and alteration of the free flow. The kinetic-energy account is retained as a plausible interpretation. A pressure rise along the surface is necessary, but its sufficient magnitude is not calculated.
The zero-thickness limit is therefore not identified with the globally inviscid sphere flow. The free-fluid and boundary-layer descriptions remain mutually coupled, and a separate translation bridge is required before the selected limiting flow pattern reaches the viscous description.
An actual field test of the limit distinction
k=epsilon^2; u=U*(1-exp(-y/epsilon)); v=-epsilon; p=0.
Both full steady momentum balances and continuity hold with actual derivatives.
0<=u<U; u(0)=0; v(0)=-epsilon is nonzero.Nondimensional suction diagnostic: tangential wall adherence does not imply normal impermeability
uniformly for y>=a>0, but not uniformly on y>0.
At y=epsilon: |u(epsilon)-U|=U*exp(-1)>0.
k*u_y(0)=U*epsilon tends to zero; k*u_yy(epsilon)=-U*exp(-1).
This replaces the former zero-thickness/unit-flow-difference scalar assignment with an actual field family. It does not reconstruct Prandtl's impermeable-wall wake or prove its flow-pattern transfer. The normal boundary data vary with epsilon; no fixed-data inviscid-limit theorem is asserted. The source's separated-flow-pattern transfer remains an explicit independent input.
The independent client in scripts/CheckIndependentReuse.lean writes its own fields with outer speed 3, viscosity epsilon^2/4 and normal velocity -epsilon/2. Public deductions check the full balances, wall shear, inner diffusion, and a nonzero defect at y=epsilon/2. This is API validation, not an independent historical-paper analysis.
Qualitative records and a controlled intervention do different work
Obstacle and curved-channel records support a qualitative flow picture only after apparatus, preparation, record, and diagram relations are supplied. They do not make the streamline drawings quantitatively accurate. The slotted-cylinder record is an independent route: suction intercepts the wall layer while preserving the background, and a mediation bridge connects that performed intervention to suppressed separation.
Only a later evidence assessment uses that result to discriminate the coupled boundary-layer model from a globally inviscid model.
The completed paper remains qualified
The complete result assembles the regime split, vorticity, boundary reduction, flat-plate calculation, separation, coupled limit, qualitative visualization, and suction intervention. Its terminal assessment keeps the quantitative separation threshold and quantitatively accurate streamline sketches unestablished. Theory/model/world transfer is a further grounding step, not a consequence of technical completion.
Complete semantic ledger
Primary theorems: shared_boundary_layer_model_retains_exact_prandtl_semantics; paper_setup_makes_shared_selected_boundary_layer_setup; prandtl_source_inputs_make_shared_boundary_layer_route_applicable; prandtl_source_inputs_realize_boundary_layer_derivational_reduction; prandtl_source_inputs_realize_source_boundary_layer_derivational_reduction; prandtl_source_inputs_realize_structural_boundary_layer_reduction; prandtl_source_inputs_realize_source_structural_boundary_layer_reduction; small_viscosity_requires_bulk_and_boundary_regime_split; free_fluid_inviscid_description_is_regime_restricted; boundary_vorticity_and_cyclic_accumulation_survive_small_viscosity; wall_adherence_and_scaling_yield_reduced_boundary_equations; boundary_layer_reduction_retains_short_surface_path_scope; established_boundary_layer_reduction_retains_steady_planar_equations; established_reduction_realizes_shared_boundary_layer_model; established_prandtl_reduction_exposes_selected_source_setup; established_shared_reduction_exposes_selected_prandtl_setup; established_prandtl_reduction_exhibits_nonvacuous_shared_boundary_layer_route; shared_boundary_layer_model_inputs_establish_prandtl_grounding; established_prandtl_reduction_and_grounding_establish_shared_result; grounded_prandtl_reduction_transfers_every_shared_claim; similarity_reduction_and_numerical_input_establish_flat_plate_drag; adverse_pressure_and_boundary_vorticity_establish_qualified_separation; separation_result_retains_necessity_without_sufficiency_claim; coupled_bulk_and_layer_descriptions_retain_selected_flow_in_limit; selected_limit_flow_figure_reaches_viscous_flow_through_bridge; water_channel_records_support_qualitative_not_quantitative_flow_picture; qualitative_visualization_supports_boundary_layer_model; targeted_layer_interception_establishes_causal_mechanistic_route; established_suction_intervention_exposes_performed_influence; suction_record_discriminates_coupled_layer_from_global_inviscid_model; paper_routes_establish_complete_prandtl_argument; complete_result_retains_open_threshold_and_qualitative_diagrams; complete_result_preserves_established_mechanism_and_open_quantification; qualified_result_realizes_every_model_claim; qualified_result_and_grounding_establish_grounded_assessment; grounded_assessment_transfers_every_claim_to_theory_and_world.
Selected countermodels: The named declarations in the current inventory distinguish small viscosity from global viscous negligibility, irrotational admissibility from preservation, reduction inputs from equations, adverse pressure from sufficient separation, and performed from merely available suction. vanishing_thickness_does_not_supply_uniform_inviscid_velocity uses the actual suction family above; it does not claim a constructed separated wake.
Physical witnesses: The vorticity countermodel retains zero initial vorticity, a nonzero boundary flux, and nonzero final vorticity. The thin-layer witness retains adherence, positive thickness/density/viscosity, and derivative-level momentum and continuity values that fail the displayed equations. Other witnesses retain positive adverse-pressure rise with nonzero wall shear, an actual shrinking viscous layer without uniform outer-velocity convergence, an inhabited streamline record outside its numerical-error bound, and an inhabited visualization with zero removed-water fraction. Thus the non-implications preserve the physical distinctions rather than relying on truth-value labels.
Coverage theorems: every_source_claim_has_semantics; small_viscosity_regime_route_is_semantically_realized; boundary_vorticity_route_is_semantically_realized; boundary_layer_reduction_route_is_semantically_realized; flat_plate_drag_route_is_semantically_realized; flow_separation_route_is_semantically_realized; coupled_singular_limit_route_is_semantically_realized; qualitative_visualization_route_is_semantically_realized; suction_intervention_route_is_semantically_realized; complete_assessment_route_is_semantically_realized; all_routes_are_semantically_realizable; route_semantic_realization_is_exhaustive.
Source-map audits: argument_wellFormed; argument_auditable; routes_wellFormed; boundary_layer_route_exposes_steady_planar_equation_formula; routes_have_exact_predecessor_graph; small_viscosity_setup_is_independent_hypothesis; calculation_contracts_are_independent_hypotheses; interpretation_scope_and_visualization_inputs_are_independent_hypotheses; suction_and_completion_scope_inputs_are_independent_hypotheses; suction_route_is_independent_of_qualitative_visualization; boundary_reduction_forks_from_regime_before_vorticity_rejoins; result_steps_apply_selected_inputs_and_contracts; dependent_routes_consume_certified_predecessor_outputs; regime_result_retains_physics_and_controlled_approximation; separation_result_retains_derivation_interpretation_and_open_scope; suction_result_retains_observation_and_interpretive_mediation; qualified_result_retains_approximation_deformation_interpretation_and_open_scope.
Atoms: smallViscosityProblemSetup, smallViscosityRegimeCalculation, establishedRegimeSplit, vorticityAndAccumulationCalculation, establishedVorticityAndAccumulation, boundaryLayerSurfacePathScope, boundaryLayerReductionCalculation, establishedBoundaryLayerReduction, steadyPlanarBoundaryLayerEquationFormula, flatPlateCalculation, establishedFlatPlateResult, separationCalculation, separationEnergyInterpretation, separationThresholdScope, establishedSeparationResult, coupledDescriptionAndLimitCalculation, establishedCoupledDescriptionAndLimit, visualizationSetup, qualitativeVisualizationCalculation, visualizationScopeAssessment, establishedQualitativeVisualization, visualizationEvidenceAssessment, visualizationModelSupport, controlledSuctionObservation, suctionMediation, suctionExplanationBridge, establishedSuctionIntervention, suctionEvidenceAssessment, suctionModelDiscrimination, completePaperResult, epistemicScopeAssessment, qualifiedCompletePaperResult.
Claims: smallViscositySetup, regimeCalculation, regimeSplit, vorticityCalculation, vorticityResult, boundaryReductionScope, boundaryReductionCalculation, boundaryReduction, boundaryEquationFormula, flatPlateCalculation, flatPlateResult, separationCalculation, separationInterpretation, separationScope, separationResult, coupledLimitCalculation, coupledLimitResult, visualizationSetup, visualizationCalculation, visualizationScope, visualizationResult, visualizationEvidence, visualizationSupport, suctionObservation, suctionMediation, suctionExplanationBridge, suctionResult, suctionEvidence, suctionDiscrimination, completeResult, epistemicScope, qualifiedResult.
Steps: stateSmallViscositySetup, supplyRegimeCalculation, deriveRegimeSplit, supplyVorticityCalculation, deriveVorticityResult, retainBoundaryReductionScope, supplyBoundaryReduction, deriveBoundaryReduction, retainBoundaryEquationFormula, supplyFlatPlateCalculation, deriveFlatPlateResult, supplySeparationCalculation, stateSeparationInterpretation, retainSeparationScope, deriveSeparationResult, supplyCoupledLimitCalculation, deriveCoupledLimitResult, stateVisualizationSetup, supplyVisualizationCalculation, retainVisualizationScope, deriveVisualizationResult, supplyVisualizationEvidence, deriveVisualizationSupport, supplySuctionObservation, stateSuctionMediation, stateSuctionExplanationBridge, deriveSuctionResult, supplySuctionEvidence, deriveSuctionDiscrimination, assembleCompleteResult, retainEpistemicScope, deriveQualifiedResult.
Routes: smallViscosityRegime, boundaryVorticity, boundaryLayerReduction, flatPlateDrag, flowSeparation, coupledSingularLimit, qualitativeVisualization, suctionIntervention, completeAssessment. Kinds: bulkBoundaryRegimeSplit, boundaryOriginAndCyclicAccumulation, thinLayerEquationReduction, similarityAndNumericalDrag, adversePressureSeparation, mutuallyCoupledDescriptionsAndSelectedLimit, waterChannelQualitativeEvidence, targetedLayerInterception, qualifiedBoundaryLayerAssessment.
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (83)
flow_directed_pressure_rise_has_aligned_velocity_and_gradient, shared_boundary_layer_model_retains_exact_prandtl_semantics, paper_setup_makes_shared_selected_boundary_layer_setup, small_viscosity_requires_bulk_and_boundary_regime_split, free_fluid_inviscid_description_is_regime_restricted, boundary_vorticity_and_cyclic_accumulation_survive_small_viscosity, wall_adherence_and_scaling_yield_reduced_boundary_equations, prandtl_source_inputs_make_shared_boundary_layer_route_applicable, prandtl_source_inputs_realize_boundary_layer_derivational_reduction, prandtl_source_inputs_realize_source_boundary_layer_derivational_reduction, prandtl_source_inputs_realize_structural_boundary_layer_reduction, prandtl_source_inputs_realize_source_structural_boundary_layer_reduction, boundary_layer_reduction_retains_short_surface_path_scope, established_boundary_layer_reduction_retains_steady_planar_equations, established_boundary_layer_reduction_retains_wall_and_outer_velocity_matching, established_reduction_realizes_shared_boundary_layer_model, established_prandtl_reduction_exposes_selected_source_setup, established_shared_reduction_exposes_selected_prandtl_setup, established_prandtl_reduction_exhibits_nonvacuous_shared_boundary_layer_route, established_prandtl_reduction_realizes_velocity_matched_boundary_layer, prandtl_boundary_layer_reduction_realizes_derivational_reduction, shared_boundary_layer_model_inputs_establish_prandtl_grounding, established_prandtl_reduction_and_grounding_establish_shared_result, grounded_prandtl_reduction_transfers_every_shared_claim, flat_plate_profile_inputs_realize_a_regular_physical_wall, flat_plate_profile_derives_the_actual_square_root_wall_shear, actual_flat_plate_profiles_establish_nonvacuous_wall_drag, similarity_reduction_and_numerical_input_establish_flat_plate_drag, the_prandtl_flat_plate_conclusion_consumes_the_actual_wall_force, the_prandtl_flat_plate_force_is_the_integral_of_its_profile_shear, boundary_vorticity_and_calculation_derive_flow_directed_pressure_rise, adverse_pressure_and_boundary_vorticity_establish_qualified_separation, established_separation_applies_pressure_necessity_to_actual_flow, separation_result_retains_necessity_without_sufficiency_claim, coupled_bulk_and_layer_descriptions_retain_selected_flow_in_limit, selected_limit_flow_figure_reaches_viscous_flow_through_bridge, water_channel_records_support_qualitative_not_quantitative_flow_picture, qualitative_visualization_supports_boundary_layer_model, targeted_layer_interception_establishes_causal_mechanistic_route, established_suction_intervention_exposes_performed_influence, suction_record_discriminates_coupled_layer_from_global_inviscid_model, paper_routes_establish_complete_prandtl_argument, complete_result_retains_open_threshold_and_qualitative_diagrams, complete_result_preserves_established_mechanism_and_open_quantification, qualified_result_realizes_every_model_claim, qualified_result_and_grounding_establish_grounded_assessment, grounded_assessment_transfers_every_claim_to_theory_and_world, selected_steady_fields_have_zero_actual_time_derivatives, actual_retained_residual_is_the_printed_steady_momentum_difference, printed_steady_equations_iff_actual_retained_balances_on_the_selected_patch, established_steady_reduction_has_an_inhabited_physical_patch, primitive_steady_balances_realize_nonvacuous_source_residual_control, steady_source_order_and_longitudinal_control_bound_the_printed_operator, planar_source_normal_balance_bounds_pressure_values_at_second_order, tangential_wall_adherence_does_not_prevent_normal_penetration, wall_adherence_does_not_supply_outer_velocity_recovery, prandtl_wall_matching_does_not_require_a_stationary_surface, small_viscosity_does_not_make_viscous_effects_globally_negligible, solving_inviscid_equations_does_not_select_the_viscous_limit, irrotational_admissibility_does_not_imply_dynamical_preservation, wall_adherence_and_thinness_do_not_perform_reduction, abstract_reduced_equation_outputs_do_not_supply_displayed_formula, small_viscosity_and_wall_adherence_do_not_supply_short_surface_path_scope, positive_coordinate_pressure_gradient_need_not_rise_along_reversed_flow, adverse_pressure_rise_need_not_be_sufficient_for_separation, vanishing_thickness_does_not_supply_uniform_inviscid_velocity, selected_flow_pattern_transfer_does_not_identify_total_descriptions, qualitative_streamline_picture_is_not_quantitative_prediction, qualitative_visualization_does_not_supply_performed_suction, available_suction_intervention_does_not_establish_performance, observed_association_without_control_does_not_establish_causal_role, local_suppression_does_not_establish_global_absence_of_separation, completed_model_does_not_transfer_without_grounding, the_actual_velocity_snapshots_are_incompressible, the_actual_profile_has_its_wall_derivative, the_profile_perturbation_has_an_actual_envelope, both_actual_wall_profiles_recover_the_same_outer_velocity, the_actual_velocity_error_is_uniformly_small, the_actual_wall_traction_uses_the_large_velocity_gradient, the_actual_one_face_force_is_the_integral_of_that_traction, the_velocity_perturbations_have_nonvacuous_actual_wall_forces, a_small_uniform_velocity_error_can_have_a_large_actual_force_error, uniform_velocity_accuracy_does_not_control_the_actual_wall_force
Coverage theorems (12)
every_source_claim_has_semantics, small_viscosity_regime_route_is_semantically_realized, boundary_vorticity_route_is_semantically_realized, boundary_layer_reduction_route_is_semantically_realized, flat_plate_drag_route_is_semantically_realized, flow_separation_route_is_semantically_realized, coupled_singular_limit_route_is_semantically_realized, qualitative_visualization_route_is_semantically_realized, suction_intervention_route_is_semantically_realized, complete_assessment_route_is_semantically_realized, all_routes_are_semantically_realizable, route_semantic_realization_is_exhaustive
Source-map audit theorems (17)
argument_wellFormed, argument_auditable, routes_wellFormed, boundary_layer_route_exposes_steady_planar_equation_formula, routes_have_exact_predecessor_graph, small_viscosity_setup_is_independent_hypothesis, calculation_contracts_are_independent_hypotheses, interpretation_scope_and_visualization_inputs_are_independent_hypotheses, suction_and_completion_scope_inputs_are_independent_hypotheses, suction_route_is_independent_of_qualitative_visualization, boundary_reduction_forks_from_regime_before_vorticity_rejoins, result_steps_apply_selected_inputs_and_contracts, dependent_routes_consume_certified_predecessor_outputs, regime_result_retains_physics_and_controlled_approximation, separation_result_retains_derivation_interpretation_and_open_scope, suction_result_retains_observation_and_interpretive_mediation, qualified_result_retains_approximation_deformation_interpretation_and_open_scope
Semantic atoms (33)
smallViscosityProblemSetup, smallViscosityRegimeCalculation, establishedRegimeSplit, vorticityAndAccumulationCalculation, establishedVorticityAndAccumulation, boundaryLayerSurfacePathScope, boundaryLayerReductionCalculation, establishedBoundaryLayerReduction, steadyPlanarBoundaryLayerEquationFormula, flatPlateCalculation, establishedFlatPlateResult, separationCalculation, directedAdversePressureRise, separationEnergyInterpretation, separationThresholdScope, establishedSeparationResult, coupledDescriptionAndLimitCalculation, establishedCoupledDescriptionAndLimit, visualizationSetup, qualitativeVisualizationCalculation, visualizationScopeAssessment, establishedQualitativeVisualization, visualizationEvidenceAssessment, visualizationModelSupport, controlledSuctionObservation, suctionMediation, suctionExplanationBridge, establishedSuctionIntervention, suctionEvidenceAssessment, suctionModelDiscrimination, completePaperResult, epistemicScopeAssessment, qualifiedCompletePaperResult
Claim identifiers (33)
smallViscositySetup, regimeCalculation, regimeSplit, vorticityCalculation, vorticityResult, boundaryReductionScope, boundaryReductionCalculation, boundaryReduction, boundaryEquationFormula, flatPlateCalculation, flatPlateResult, separationCalculation, directedPressureRise, separationInterpretation, separationScope, separationResult, coupledLimitCalculation, coupledLimitResult, visualizationSetup, visualizationCalculation, visualizationScope, visualizationResult, visualizationEvidence, visualizationSupport, suctionObservation, suctionMediation, suctionExplanationBridge, suctionResult, suctionEvidence, suctionDiscrimination, completeResult, epistemicScope, qualifiedResult
Step identifiers (33)
stateSmallViscositySetup, supplyRegimeCalculation, deriveRegimeSplit, supplyVorticityCalculation, deriveVorticityResult, retainBoundaryReductionScope, supplyBoundaryReduction, deriveBoundaryReduction, retainBoundaryEquationFormula, supplyFlatPlateCalculation, deriveFlatPlateResult, supplySeparationCalculation, deriveDirectedPressureRise, stateSeparationInterpretation, retainSeparationScope, deriveSeparationResult, supplyCoupledLimitCalculation, deriveCoupledLimitResult, stateVisualizationSetup, supplyVisualizationCalculation, retainVisualizationScope, deriveVisualizationResult, supplyVisualizationEvidence, deriveVisualizationSupport, supplySuctionObservation, stateSuctionMediation, stateSuctionExplanationBridge, deriveSuctionResult, supplySuctionEvidence, deriveSuctionDiscrimination, assembleCompleteResult, retainEpistemicScope, deriveQualifiedResult
Route identifiers (9)
smallViscosityRegime, boundaryVorticity, boundaryLayerReduction, flatPlateDrag, flowSeparation, coupledSingularLimit, qualitativeVisualization, suctionIntervention, completeAssessment
Route kinds (9)
bulkBoundaryRegimeSplit, boundaryOriginAndCyclicAccumulation, thinLayerEquationReduction, similarityAndNumericalDrag, adversePressureSeparation, mutuallyCoupledDescriptionsAndSelectedLimit, waterChannelQualitativeEvidence, targetedLayerInterception, qualifiedBoundaryLayerAssessment
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.
smallViscosityRegime
Logical kind: bulkBoundaryRegimeSplit.
Required predecessor routes: none.
Ordered inference steps: stateSmallViscositySetup, supplyRegimeCalculation, deriveRegimeSplit.
Exported conclusions: regimeSplit.
boundaryVorticity
Logical kind: boundaryOriginAndCyclicAccumulation.
Required predecessor routes: smallViscosityRegime.
Ordered inference steps: supplyVorticityCalculation, deriveVorticityResult.
Exported conclusions: vorticityResult.
boundaryLayerReduction
Logical kind: thinLayerEquationReduction.
Required predecessor routes: smallViscosityRegime.
Ordered inference steps: retainBoundaryReductionScope, supplyBoundaryReduction, deriveBoundaryReduction, retainBoundaryEquationFormula.
Exported conclusions: boundaryEquationFormula, boundaryReduction.
flatPlateDrag
Logical kind: similarityAndNumericalDrag.
Required predecessor routes: boundaryLayerReduction.
Ordered inference steps: supplyFlatPlateCalculation, deriveFlatPlateResult.
Exported conclusions: flatPlateResult.
flowSeparation
Logical kind: adversePressureSeparation.
Required predecessor routes: boundaryLayerReduction, boundaryVorticity.
Ordered inference steps: supplySeparationCalculation, deriveDirectedPressureRise, stateSeparationInterpretation, retainSeparationScope, deriveSeparationResult.
Exported conclusions: separationResult, separationInterpretation, separationScope.
coupledSingularLimit
Logical kind: mutuallyCoupledDescriptionsAndSelectedLimit.
Required predecessor routes: flowSeparation.
Ordered inference steps: supplyCoupledLimitCalculation, deriveCoupledLimitResult.
Exported conclusions: coupledLimitResult.
qualitativeVisualization
Logical kind: waterChannelQualitativeEvidence.
Required predecessor routes: coupledSingularLimit.
Ordered inference steps: stateVisualizationSetup, supplyVisualizationCalculation, retainVisualizationScope, deriveVisualizationResult, supplyVisualizationEvidence, deriveVisualizationSupport.
Exported conclusions: visualizationResult, visualizationSupport, visualizationScope.
suctionIntervention
Logical kind: targetedLayerInterception.
Required predecessor routes: none.
Ordered inference steps: supplySuctionObservation, stateSuctionMediation, stateSuctionExplanationBridge, deriveSuctionResult, supplySuctionEvidence, deriveSuctionDiscrimination.
Exported conclusions: suctionResult, suctionDiscrimination.
completeAssessment
Logical kind: qualifiedBoundaryLayerAssessment.
Required predecessor routes: smallViscosityRegime, boundaryVorticity, boundaryLayerReduction, flatPlateDrag, flowSeparation, coupledSingularLimit, qualitativeVisualization, suctionIntervention.
Ordered inference steps: assembleCompleteResult, retainEpistemicScope, deriveQualifiedResult.
Exported conclusions: qualifiedResult, completeResult, epistemicScope.